copsexg

Description: Substitution of class A for ordered pair <. x , y >. . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker copsexgw when possible. (Contributed by NM, 27-Dec-1996) (Revised by Andrew Salmon, 11-Jul-2011) (Proof shortened by Wolf Lammen, 25-Aug-2019) (New usage is discouraged.)

		Ref	Expression
	Assertion	copsexg	$⊢ 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	$⊢ \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ) \to \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ)$
5	4	19.23bi	$⊢ (⟨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	drex1	$⊢ \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		nfeqf2	$⊢ \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		ax12ev2c	$⊢ z = x \to (\exists x (z = x \land \exists y (w = y \land φ)) \to \exists y (w = y \land φ))$
33		ax12ev2c	$⊢ w = y \to (\exists y (w = y \land φ) \to φ)$
34	32 33	sylan9	$⊢ (z = x \land w = y) \to (\exists x (z = x \land \exists y (w = y \land φ)) \to φ)$
35	31 34	syl5	$⊢ (z = x \land w = y) \to (\exists x \exists y ((z = x \land w = y) \land φ) \to φ)$
36	11 35	biimtrid	$⊢ (z = x \land w = y) \to (\exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ) \to φ)$
37	9 36	sylbi	$⊢ ⟨z, w⟩ = ⟨x, y⟩ \to (\exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ) \to φ)$
38	6 37	impbid	$⊢ ⟨z, w⟩ = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ))$
39		eqeq1	$⊢ A = ⟨z, w⟩ \to (A = ⟨x, y⟩ \leftrightarrow ⟨z, w⟩ = ⟨x, y⟩)$
40	39	anbi1d	$⊢ A = ⟨z, w⟩ \to ((A = ⟨x, y⟩ \land φ) \leftrightarrow (⟨z, w⟩ = ⟨x, y⟩ \land φ))$
41	40	2exbidv	$⊢ A = ⟨z, w⟩ \to (\exists x \exists y (A = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y (⟨z, w⟩ = ⟨x, y⟩ \land φ))$
42	41	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 φ)))$
43	39 42	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 φ))))$
44	38 43	mpbiri	$⊢ A = ⟨z, w⟩ \to (A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)))$
45	44	adantr	$⊢ (A = ⟨z, w⟩ \land ⟨z, w⟩ = ⟨x, y⟩) \to (A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)))$
46	45	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 φ)))$
47	3 46	sylbi	$⊢ A = ⟨x, y⟩ \to (A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ)))$
48	47	pm2.43i	$⊢ A = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land φ))$

Metamath Proof Explorer

Theorem copsexg

Proof