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		euequ	$⊢ \exists! x x = z$
18		equcom	$⊢ x = z \leftrightarrow z = x$
19	18	eubii	$⊢ \exists! x x = z \leftrightarrow \exists! x z = x$
20	17 19	mpbi	$⊢ \exists! x z = x$
21		eupick	$⊢ (\exists! x z = x \land \exists x (z = x \land \exists y (w = y \land φ))) \to (z = x \to \exists y (w = y \land φ))$
22	20 21	mpan	$⊢ \exists x (z = x \land \exists y (w = y \land φ)) \to (z = x \to \exists y (w = y \land φ))$
23	22	com12	$⊢ z = x \to (\exists x (z = x \land \exists y (w = y \land φ)) \to \exists y (w = y \land φ))$
24		euequ	$⊢ \exists! y y = w$
25		equcom	$⊢ y = w \leftrightarrow w = y$
26	25	eubii	$⊢ \exists! y y = w \leftrightarrow \exists! y w = y$
27	24 26	mpbi	$⊢ \exists! y w = y$
28		eupick	$⊢ (\exists! y w = y \land \exists y (w = y \land φ)) \to (w = y \to φ)$
29	27 28	mpan	$⊢ \exists y (w = y \land φ) \to (w = y \to φ)$
30	29	com12	$⊢ w = y \to (\exists y (w = y \land φ) \to φ)$
31	23 30	sylan9	$⊢ (z = x \land w = y) \to (\exists x (z = x \land \exists y (w = y \land φ)) \to φ)$
32	16 31	biimtrid	$⊢ (z = x \land w = y) \to (\exists x \exists y ((z = x \land w = y) \land φ) \to φ)$
33	11 32	biimtrid	$⊢ (z = x \land w = y) \to (\exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ) \to φ)$
34	9 33	sylbi	$⊢ ⟨z, w⟩ = ⟨x, y⟩ \to (\exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ) \to φ)$
35	6 34	impbid	$⊢ ⟨z, w⟩ = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ))$
36		eqeq1	$⊢ A = ⟨z, w⟩ \to (A = ⟨x, y⟩ \leftrightarrow ⟨z, w⟩ = ⟨x, y⟩)$
37	36	anbi1d	$⊢ A = ⟨z, w⟩ \to ((A = ⟨x, y⟩ \land φ) \leftrightarrow (⟨z, w⟩ = ⟨x, y⟩ \land φ))$
38	37	2exbidv	$⊢ A = ⟨z, w⟩ \to (\exists x \exists y (A = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ))$
39	38	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 φ)))$
40	36 39	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 φ))))$
41	35 40	mpbiri	$⊢ A = ⟨z, w⟩ \to (A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)))$
42	41	adantr	$⊢ (A = ⟨z, w⟩ \land ⟨z, w⟩ = ⟨x, y⟩) \to (A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)))$
43	42	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 φ)))$
44	3 43	sylbi	$⊢ A = ⟨x, y⟩ \to (A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)))$
45	44	pm2.43i	$⊢ A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ))$

Metamath Proof Explorer

Theorem copsexgw

Proof