Theorem copsexg 3999

Description: Substitution of class 𝐴 for ordered pair ⟨𝑥, 𝑦⟩. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.)

Assertion

Ref	Expression
copsexg	⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem copsexg

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2604	. . . 4 ⊢ 𝑥 ∈ V
2		vex 2604	. . . 4 ⊢ 𝑦 ∈ V
3	1, 2	eqvinop 3998	. . 3 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑧∃𝑤(𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
4		19.8a 1522	. . . . . . . . 9 ⊢ (∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
5	4	19.23bi 1523	. . . . . . . 8 ⊢ ((⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
6	5	ex 113	. . . . . . 7 ⊢ (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 → ∃𝑥∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
7		vex 2604	. . . . . . . . 9 ⊢ 𝑧 ∈ V
8		vex 2604	. . . . . . . . 9 ⊢ 𝑤 ∈ V
9	7, 8	opth 3992	. . . . . . . 8 ⊢ (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦))
10	9	anbi1i 445	. . . . . . . . . 10 ⊢ ((⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑))
11	10	2exbii 1537	. . . . . . . . 9 ⊢ (∃𝑥∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑))
12		nfe1 1425	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))
13		dveeq2or 1737	. . . . . . . . . . . 12 ⊢ (∀𝑦 𝑦 = 𝑥 ∨ Ⅎ𝑦 𝑧 = 𝑥)
14		nfae 1647	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦∀𝑦 𝑦 = 𝑥
15		anass 393	. . . . . . . . . . . . . . . 16 ⊢ (((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) ↔ (𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑)))
16		19.8a 1522	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 = 𝑦 ∧ 𝜑) → ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))
17	16	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 𝑦 = 𝑥 → ((𝑤 = 𝑦 ∧ 𝜑) → ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))
18	17	anim2d 330	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 𝑦 = 𝑥 → ((𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))))
19	15, 18	syl5bi 150	. . . . . . . . . . . . . . 15 ⊢ (∀𝑦 𝑦 = 𝑥 → (((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))))
20	14, 19	eximd 1543	. . . . . . . . . . . . . 14 ⊢ (∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑦(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))))
21		biidd 170	. . . . . . . . . . . . . . 15 ⊢ (∀𝑦 𝑦 = 𝑥 → ((𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) ↔ (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))))
22	21	drex1 1719	. . . . . . . . . . . . . 14 ⊢ (∀𝑦 𝑦 = 𝑥 → (∃𝑦(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) ↔ ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))))
23	20, 22	sylibd 147	. . . . . . . . . . . . 13 ⊢ (∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))))
24	15	exbii 1536	. . . . . . . . . . . . . . 15 ⊢ (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) ↔ ∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑)))
25		19.40 1562	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑)) → (∃𝑦 𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))
26		19.9t 1573	. . . . . . . . . . . . . . . . . 18 ⊢ (Ⅎ𝑦 𝑧 = 𝑥 → (∃𝑦 𝑧 = 𝑥 ↔ 𝑧 = 𝑥))
27	26	biimpd 142	. . . . . . . . . . . . . . . . 17 ⊢ (Ⅎ𝑦 𝑧 = 𝑥 → (∃𝑦 𝑧 = 𝑥 → 𝑧 = 𝑥))
28	27	anim1d 329	. . . . . . . . . . . . . . . 16 ⊢ (Ⅎ𝑦 𝑧 = 𝑥 → ((∃𝑦 𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))))
29	25, 28	syl5 32	. . . . . . . . . . . . . . 15 ⊢ (Ⅎ𝑦 𝑧 = 𝑥 → (∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))))
30	24, 29	syl5bi 150	. . . . . . . . . . . . . 14 ⊢ (Ⅎ𝑦 𝑧 = 𝑥 → (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))))
31		19.8a 1522	. . . . . . . . . . . . . 14 ⊢ ((𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))
32	30, 31	syl6 33	. . . . . . . . . . . . 13 ⊢ (Ⅎ𝑦 𝑧 = 𝑥 → (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))))
33	23, 32	jaoi 668	. . . . . . . . . . . 12 ⊢ ((∀𝑦 𝑦 = 𝑥 ∨ Ⅎ𝑦 𝑧 = 𝑥) → (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))))
34	13, 33	ax-mp 7	. . . . . . . . . . 11 ⊢ (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))
35	12, 34	exlimi 1525	. . . . . . . . . 10 ⊢ (∃𝑥∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))
36		euequ1 2036	. . . . . . . . . . . . . 14 ⊢ ∃!𝑥 𝑥 = 𝑧
37		equcom 1633	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 ↔ 𝑧 = 𝑥)
38	37	eubii 1950	. . . . . . . . . . . . . 14 ⊢ (∃!𝑥 𝑥 = 𝑧 ↔ ∃!𝑥 𝑧 = 𝑥)
39	36, 38	mpbi 143	. . . . . . . . . . . . 13 ⊢ ∃!𝑥 𝑧 = 𝑥
40		eupick 2020	. . . . . . . . . . . . 13 ⊢ ((∃!𝑥 𝑧 = 𝑥 ∧ ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) → (𝑧 = 𝑥 → ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))
41	39, 40	mpan 414	. . . . . . . . . . . 12 ⊢ (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → (𝑧 = 𝑥 → ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))
42	41	com12 30	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))
43		euequ1 2036	. . . . . . . . . . . . . 14 ⊢ ∃!𝑦 𝑦 = 𝑤
44		equcom 1633	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑤 ↔ 𝑤 = 𝑦)
45	44	eubii 1950	. . . . . . . . . . . . . 14 ⊢ (∃!𝑦 𝑦 = 𝑤 ↔ ∃!𝑦 𝑤 = 𝑦)
46	43, 45	mpbi 143	. . . . . . . . . . . . 13 ⊢ ∃!𝑦 𝑤 = 𝑦
47		eupick 2020	. . . . . . . . . . . . 13 ⊢ ((∃!𝑦 𝑤 = 𝑦 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → (𝑤 = 𝑦 → 𝜑))
48	46, 47	mpan 414	. . . . . . . . . . . 12 ⊢ (∃𝑦(𝑤 = 𝑦 ∧ 𝜑) → (𝑤 = 𝑦 → 𝜑))
49	48	com12 30	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑦 → (∃𝑦(𝑤 = 𝑦 ∧ 𝜑) → 𝜑))
50	42, 49	sylan9 401	. . . . . . . . . 10 ⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → 𝜑))
51	35, 50	syl5 32	. . . . . . . . 9 ⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (∃𝑥∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → 𝜑))
52	11, 51	syl5bi 150	. . . . . . . 8 ⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (∃𝑥∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝜑))
53	9, 52	sylbi 119	. . . . . . 7 ⊢ (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (∃𝑥∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝜑))
54	6, 53	impbid 127	. . . . . 6 ⊢ (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
55		eqeq1 2087	. . . . . . 7 ⊢ (𝐴 = ⟨𝑧, 𝑤⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
56	55	anbi1d 452	. . . . . . . . 9 ⊢ (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
57	56	2exbidv 1789	. . . . . . . 8 ⊢ (𝐴 = ⟨𝑧, 𝑤⟩ → (∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
58	57	bibi2d 230	. . . . . . 7 ⊢ (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ (𝜑 ↔ ∃𝑥∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
59	55, 58	imbi12d 232	. . . . . 6 ⊢ (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))) ↔ (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))))
60	54, 59	mpbiri 166	. . . . 5 ⊢ (𝐴 = ⟨𝑧, 𝑤⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
61	60	adantr 270	. . . 4 ⊢ ((𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
62	61	exlimivv 1817	. . 3 ⊢ (∃𝑧∃𝑤(𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
63	3, 62	sylbi 119	. 2 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
64	63	pm2.43i 48	1 ⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   ∨ wo 661  ∀wal 1282   = wceq 1284  Ⅎwnf 1389  ∃wex 1421  ∃!weu 1941  ⟨cop 3401

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-pow 3948  ax-pr 3964

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-un 2977  df-in 2979  df-ss 2986  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407

This theorem is referenced by:  copsex2t  4000  copsex2g  4001  opabid  4012  mosubopt  4423