copsex2gd

Description: Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995) Use a similar proof to copsex4g to reduce axiom usage. (Revised by SN, 1-Sep-2024) Adapt copsex2g $p to deduction form. (Revised by BJ, 28-Mar-2026) Do not use copsex2g . (Proof modification is discouraged.)

		Ref	Expression
	Hypothesis	copsex2gd.is	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
	Assertion	copsex2gd	$⊢ (φ \land (A \in V \land B \in W)) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ)$

Proof

Step	Hyp	Ref	Expression
1		copsex2gd.is	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
2		eqcom	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \leftrightarrow ⟨x, y⟩ = ⟨A, B⟩$
3		vex	$⊢ x \in V$
4		vex	$⊢ y \in V$
5	3 4	opth	$⊢ ⟨x, y⟩ = ⟨A, B⟩ \leftrightarrow (x = A \land y = B)$
6	2 5	bitri	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \leftrightarrow (x = A \land y = B)$
7	6	anbi1i	$⊢ (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow ((x = A \land y = B) \land ψ)$
8	7	2exbii	$⊢ \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow \exists x \exists y ((x = A \land y = B) \land ψ)$
9		simpr	$⊢ (φ \land (x = A \land y = B)) \to (x = A \land y = B)$
10	9 1	cgsex2gd	$⊢ (φ \land (A \in V \land B \in W)) \to (\exists x \exists y ((x = A \land y = B) \land ψ) \leftrightarrow χ)$
11	8 10	bitrid	$⊢ (φ \land (A \in V \land B \in W)) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ)$

Metamath Proof Explorer

Theorem copsex2gd

Proof