copsexgw

Description: Version of copsexg with a disjoint variable condition, which does not require ax-13 . (Contributed by Gino Giotto, 26-Jan-2024)

		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		nfe1	$⊢ Ⅎ x \exists x (z = x \land \exists y (w = y \land φ))$
13		19.8a	$⊢ (w = y \land φ) \to \exists y (w = y \land φ)$
14	13	anim2i	$⊢ (z = x \land (w = y \land φ)) \to (z = x \land \exists y (w = y \land φ))$
15	14	anassrs	$⊢ ((z = x \land w = y) \land φ) \to (z = x \land \exists y (w = y \land φ))$
16	15	eximi	$⊢ \exists y ((z = x \land w = y) \land φ) \to \exists y (z = x \land \exists y (w = y \land φ))$
17		biidd	$⊢ \forall y y = x \to ((z = x \land \exists y (w = y \land φ)) \leftrightarrow (z = x \land \exists y (w = y \land φ)))$
18	17	drex1v	$⊢ \forall y y = x \to (\exists y (z = x \land \exists y (w = y \land φ)) \leftrightarrow \exists x (z = x \land \exists y (w = y \land φ)))$
19	16 18	imbitrid	$⊢ \forall y y = x \to (\exists y ((z = x \land w = y) \land φ) \to \exists x (z = x \land \exists y (w = y \land φ)))$
20		anass	$⊢ ((z = x \land w = y) \land φ) \leftrightarrow (z = x \land (w = y \land φ))$
21	20	exbii	$⊢ \exists y ((z = x \land w = y) \land φ) \leftrightarrow \exists y (z = x \land (w = y \land φ))$
22		19.40	$⊢ \exists y (z = x \land (w = y \land φ)) \to (\exists y z = x \land \exists y (w = y \land φ))$
23		nfvd	$⊢ \neg \forall y y = x \to Ⅎ y z = x$
24	23	19.9d	$⊢ \neg \forall y y = x \to (\exists y z = x \to z = x)$
25	24	anim1d	$⊢ \neg \forall y y = x \to ((\exists y z = x \land \exists y (w = y \land φ)) \to (z = x \land \exists y (w = y \land φ)))$
26	22 25	syl5	$⊢ \neg \forall y y = x \to (\exists y (z = x \land (w = y \land φ)) \to (z = x \land \exists y (w = y \land φ)))$
27	21 26	biimtrid	$⊢ \neg \forall y y = x \to (\exists y ((z = x \land w = y) \land φ) \to (z = x \land \exists y (w = y \land φ)))$
28		19.8a	$⊢ (z = x \land \exists y (w = y \land φ)) \to \exists x (z = x \land \exists y (w = y \land φ))$
29	27 28	syl6	$⊢ \neg \forall y y = x \to (\exists y ((z = x \land w = y) \land φ) \to \exists x (z = x \land \exists y (w = y \land φ)))$
30	19 29	pm2.61i	$⊢ \exists y ((z = x \land w = y) \land φ) \to \exists x (z = x \land \exists y (w = y \land φ))$
31	12 30	exlimi	$⊢ \exists x \exists y ((z = x \land w = y) \land φ) \to \exists x (z = x \land \exists y (w = y \land φ))$
32		euequ	$⊢ \exists! x x = z$
33		equcom	$⊢ x = z \leftrightarrow z = x$
34	33	eubii	$⊢ \exists! x x = z \leftrightarrow \exists! x z = x$
35	32 34	mpbi	$⊢ \exists! x z = x$
36		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 φ))$
37	35 36	mpan	$⊢ \exists x (z = x \land \exists y (w = y \land φ)) \to (z = x \to \exists y (w = y \land φ))$
38	37	com12	$⊢ z = x \to (\exists x (z = x \land \exists y (w = y \land φ)) \to \exists y (w = y \land φ))$
39		euequ	$⊢ \exists! y y = w$
40		equcom	$⊢ y = w \leftrightarrow w = y$
41	40	eubii	$⊢ \exists! y y = w \leftrightarrow \exists! y w = y$
42	39 41	mpbi	$⊢ \exists! y w = y$
43		eupick	$⊢ (\exists! y w = y \land \exists y (w = y \land φ)) \to (w = y \to φ)$
44	42 43	mpan	$⊢ \exists y (w = y \land φ) \to (w = y \to φ)$
45	44	com12	$⊢ w = y \to (\exists y (w = y \land φ) \to φ)$
46	38 45	sylan9	$⊢ (z = x \land w = y) \to (\exists x (z = x \land \exists y (w = y \land φ)) \to φ)$
47	31 46	syl5	$⊢ (z = x \land w = y) \to (\exists x \exists y ((z = x \land w = y) \land φ) \to φ)$
48	11 47	biimtrid	$⊢ (z = x \land w = y) \to (\exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ) \to φ)$
49	9 48	sylbi	$⊢ ⟨z, w⟩ = ⟨x, y⟩ \to (\exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ) \to φ)$
50	6 49	impbid	$⊢ ⟨z, w⟩ = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ))$
51		eqeq1	$⊢ A = ⟨z, w⟩ \to (A = ⟨x, y⟩ \leftrightarrow ⟨z, w⟩ = ⟨x, y⟩)$
52	51	anbi1d	$⊢ A = ⟨z, w⟩ \to ((A = ⟨x, y⟩ \land φ) \leftrightarrow (⟨z, w⟩ = ⟨x, y⟩ \land φ))$
53	52	2exbidv	$⊢ A = ⟨z, w⟩ \to (\exists x \exists y (A = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ))$
54	53	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 φ)))$
55	51 54	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 φ))))$
56	50 55	mpbiri	$⊢ A = ⟨z, w⟩ \to (A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)))$
57	56	adantr	$⊢ (A = ⟨z, w⟩ \land ⟨z, w⟩ = ⟨x, y⟩) \to (A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)))$
58	57	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 φ)))$
59	3 58	sylbi	$⊢ A = ⟨x, y⟩ \to (A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)))$
60	59	pm2.43i	$⊢ A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ))$

Metamath Proof Explorer

Theorem copsexgw

Proof