copsexgw

Description: Version of copsexg with a disjoint variable condition, which does not require ax-13 . (Contributed by GG, 26-Jan-2024) Shorten proof and remove dependency on ax-10 . (Revised by Eric Schmidt, 2-May-2026)

		Ref	Expression
	Assertion	copsexgw	$⊢ A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ))$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		vex	$⊢ y \in V$
3	1 2	eqvinop	$⊢ A = ⟨x, y⟩ \leftrightarrow \exists z \exists w (A = ⟨z, w⟩ \land ⟨z, w⟩ = ⟨x, y⟩)$
4		19.8a	$⊢ (⟨z, w⟩ = ⟨x, y⟩ \land φ) \to \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ)$
5	4	19.8ad	$⊢ (⟨z, w⟩ = ⟨x, y⟩ \land φ) \to \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ)$
6	5	ex	$⊢ ⟨z, w⟩ = ⟨x, y⟩ \to (φ \to \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ))$
7		vex	$⊢ z \in V$
8		vex	$⊢ w \in V$
9	7 8	opth	$⊢ ⟨z, w⟩ = ⟨x, y⟩ \leftrightarrow (z = x \land w = y)$
10	9	anbi1i	$⊢ (⟨z, w⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ((z = x \land w = y) \land φ)$
11	10	2exbii	$⊢ \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y ((z = x \land w = y) \land φ)$
12		anass	$⊢ ((z = x \land w = y) \land φ) \leftrightarrow (z = x \land (w = y \land φ))$
13	12	exbii	$⊢ \exists y ((z = x \land w = y) \land φ) \leftrightarrow \exists y (z = x \land (w = y \land φ))$
14		19.42v	$⊢ \exists y (z = x \land (w = y \land φ)) \leftrightarrow (z = x \land \exists y (w = y \land φ))$
15	13 14	bitri	$⊢ \exists y ((z = x \land w = y) \land φ) \leftrightarrow (z = x \land \exists y (w = y \land φ))$
16	15	exbii	$⊢ \exists x \exists y ((z = x \land w = y) \land φ) \leftrightarrow \exists x (z = x \land \exists y (w = y \land φ))$
17		ax12ev2c	$⊢ z = x \to (\exists x (z = x \land \exists y (w = y \land φ)) \to \exists y (w = y \land φ))$
18		ax12ev2c	$⊢ w = y \to (\exists y (w = y \land φ) \to φ)$
19	17 18	sylan9	$⊢ (z = x \land w = y) \to (\exists x (z = x \land \exists y (w = y \land φ)) \to φ)$
20	16 19	biimtrid	$⊢ (z = x \land w = y) \to (\exists x \exists y ((z = x \land w = y) \land φ) \to φ)$
21	11 20	biimtrid	$⊢ (z = x \land w = y) \to (\exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ) \to φ)$
22	9 21	sylbi	$⊢ ⟨z, w⟩ = ⟨x, y⟩ \to (\exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ) \to φ)$
23	6 22	impbid	$⊢ ⟨z, w⟩ = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ))$
24		eqeq1	$⊢ A = ⟨z, w⟩ \to (A = ⟨x, y⟩ \leftrightarrow ⟨z, w⟩ = ⟨x, y⟩)$
25	24	anbi1d	$⊢ A = ⟨z, w⟩ \to ((A = ⟨x, y⟩ \land φ) \leftrightarrow (⟨z, w⟩ = ⟨x, y⟩ \land φ))$
26	25	2exbidv	$⊢ A = ⟨z, w⟩ \to (\exists x \exists y (A = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ))$
27	26	bibi2d	$⊢ A = ⟨z, w⟩ \to ((φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)) \leftrightarrow (φ \leftrightarrow \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ)))$
28	24 27	imbi12d	$⊢ A = ⟨z, w⟩ \to ((A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ))) \leftrightarrow (⟨z, w⟩ = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ))))$
29	23 28	mpbiri	$⊢ A = ⟨z, w⟩ \to (A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)))$
30	29	adantr	$⊢ (A = ⟨z, w⟩ \land ⟨z, w⟩ = ⟨x, y⟩) \to (A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)))$
31	30	exlimivv	$⊢ \exists z \exists w (A = ⟨z, w⟩ \land ⟨z, w⟩ = ⟨x, y⟩) \to (A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)))$
32	3 31	sylbi	$⊢ A = ⟨x, y⟩ \to (A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)))$
33	32	pm2.43i	$⊢ A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ))$

Metamath Proof Explorer

Theorem copsexgw

Proof