写像の定理証明の推論の疑問

f(A)=pY(G∩(A×Y))の証明の途中に ∃x((x, b) ∈ G∩ (A×Y)) ⇒∃x((x, b) ∈ G∩ (A×Y) ∧ b = pY(x, b)) で付け足されたのがあるんですけどこれどういう推論規則？で付け足されてるのでしょうか？ ∃x(P(x)∧Q(x))⇒∃x(P(x))みたいな推論があるならわかるんですけどこれこの逆ですよね。だから他のやり方だと思うんですけどわかんなくて、付け足されたのが真だから∧でつけても真理値変わらないからいいってことなんですかね？ならその推論規則？はどのような論理式？で表せるのでしょうか？

その本では、厳密な論理体系が指定されていますか？特に指定がなければ、「付け足されたのが真だから∧でつけても真理値変わらないからいい」という理解で十分だと思います。 $P(x)$ を $(x,b) \in G \cap (A \times Y)$、$Q(x)$ を $b=p_Y(x,b)$ とすると、$\exists x (P(x))$ と $\forall x (Q(x))$ から $\exists x (P(x) \land Q(x))$ を導くといった変形が行われています。 もし、この変形が正しいことを述語論理の自然演繹で証明したいのであれば、$\forall$-除去、$\land$-導入、$\exists$-導入、$\exists$-除去といった推論規則を組み合わせる必要があります。 ご不明な点や、さらに詳しい説明が必要な場合は、お気軽にコメントでご質問ください。 $\textbf{\textsf{（追記: 2025年8月28日13:18）}}$ コメントへの返答です。 はい、右の要素を返す射影 $p_Y$ は、左の要素に依存しませんので、$Q(x)$ を全称化することができます。射影の定義域を考慮して、より正確には $\forall x \in X(Q(x))$ と全称化されます。自然演繹の厳密さが必要であれば、$\forall$-導入の適用条件が満たされていることを確認してください。$P(x)$ から $x \in X$ を導出できるため、結果的に $x \in X$ の部分は無視することができます。これで、あなたの疑問に答えられているでしょうか？