MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  copsexg Structured version   Visualization version   GIF version

Theorem copsexg 5083
Description: Substitution of class 𝐴 for ordered pair 𝑥, 𝑦. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 25-Aug-2019.)
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.
StepHypRef Expression
1 vex 3354 . . . 4 𝑥 ∈ V
2 vex 3354 . . . 4 𝑦 ∈ V
31, 2eqvinop 5082 . . 3 (𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑧𝑤(𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
4 19.8a 2206 . . . . . . . . 9 (∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
5419.23bi 2215 . . . . . . . 8 ((⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
65ex 397 . . . . . . 7 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 → ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
7 vex 3354 . . . . . . . . 9 𝑧 ∈ V
8 vex 3354 . . . . . . . . 9 𝑤 ∈ V
97, 8opth 5072 . . . . . . . 8 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝑧 = 𝑥𝑤 = 𝑦))
109anbi1i 610 . . . . . . . . . 10 ((⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑))
11102exbii 1925 . . . . . . . . 9 (∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑))
12 nfe1 2183 . . . . . . . . . . 11 𝑥𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))
13 19.8a 2206 . . . . . . . . . . . . . . . 16 ((𝑤 = 𝑦𝜑) → ∃𝑦(𝑤 = 𝑦𝜑))
1413anim2i 603 . . . . . . . . . . . . . . 15 ((𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
1514anassrs 453 . . . . . . . . . . . . . 14 (((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
1615eximi 1910 . . . . . . . . . . . . 13 (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑦(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
17 biidd 252 . . . . . . . . . . . . . 14 (∀𝑦 𝑦 = 𝑥 → ((𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) ↔ (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
1817drex1 2477 . . . . . . . . . . . . 13 (∀𝑦 𝑦 = 𝑥 → (∃𝑦(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) ↔ ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
1916, 18syl5ib 234 . . . . . . . . . . . 12 (∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
20 anass 454 . . . . . . . . . . . . . . 15 (((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) ↔ (𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)))
2120exbii 1924 . . . . . . . . . . . . . 14 (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) ↔ ∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)))
22 19.40 1948 . . . . . . . . . . . . . . 15 (∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)) → (∃𝑦 𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
23 nfeqf2 2452 . . . . . . . . . . . . . . . . 17 (¬ ∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦 𝑧 = 𝑥)
242319.9d 2225 . . . . . . . . . . . . . . . 16 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦 𝑧 = 𝑥𝑧 = 𝑥))
2524anim1d 598 . . . . . . . . . . . . . . 15 (¬ ∀𝑦 𝑦 = 𝑥 → ((∃𝑦 𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
2622, 25syl5 34 . . . . . . . . . . . . . 14 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
2721, 26syl5bi 232 . . . . . . . . . . . . 13 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
28 19.8a 2206 . . . . . . . . . . . . 13 ((𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
2927, 28syl6 35 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
3019, 29pm2.61i 176 . . . . . . . . . . 11 (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
3112, 30exlimi 2242 . . . . . . . . . 10 (∃𝑥𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
32 euequ1 2624 . . . . . . . . . . . . . 14 ∃!𝑥 𝑥 = 𝑧
33 equcom 2103 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧𝑧 = 𝑥)
3433eubii 2640 . . . . . . . . . . . . . 14 (∃!𝑥 𝑥 = 𝑧 ↔ ∃!𝑥 𝑧 = 𝑥)
3532, 34mpbi 220 . . . . . . . . . . . . 13 ∃!𝑥 𝑧 = 𝑥
36 eupick 2685 . . . . . . . . . . . . 13 ((∃!𝑥 𝑧 = 𝑥 ∧ ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))) → (𝑧 = 𝑥 → ∃𝑦(𝑤 = 𝑦𝜑)))
3735, 36mpan 670 . . . . . . . . . . . 12 (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 → ∃𝑦(𝑤 = 𝑦𝜑)))
3837com12 32 . . . . . . . . . . 11 (𝑧 = 𝑥 → (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → ∃𝑦(𝑤 = 𝑦𝜑)))
39 euequ1 2624 . . . . . . . . . . . . . 14 ∃!𝑦 𝑦 = 𝑤
40 equcom 2103 . . . . . . . . . . . . . . 15 (𝑦 = 𝑤𝑤 = 𝑦)
4140eubii 2640 . . . . . . . . . . . . . 14 (∃!𝑦 𝑦 = 𝑤 ↔ ∃!𝑦 𝑤 = 𝑦)
4239, 41mpbi 220 . . . . . . . . . . . . 13 ∃!𝑦 𝑤 = 𝑦
43 eupick 2685 . . . . . . . . . . . . 13 ((∃!𝑦 𝑤 = 𝑦 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → (𝑤 = 𝑦𝜑))
4442, 43mpan 670 . . . . . . . . . . . 12 (∃𝑦(𝑤 = 𝑦𝜑) → (𝑤 = 𝑦𝜑))
4544com12 32 . . . . . . . . . . 11 (𝑤 = 𝑦 → (∃𝑦(𝑤 = 𝑦𝜑) → 𝜑))
4638, 45sylan9 497 . . . . . . . . . 10 ((𝑧 = 𝑥𝑤 = 𝑦) → (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → 𝜑))
4731, 46syl5 34 . . . . . . . . 9 ((𝑧 = 𝑥𝑤 = 𝑦) → (∃𝑥𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → 𝜑))
4811, 47syl5bi 232 . . . . . . . 8 ((𝑧 = 𝑥𝑤 = 𝑦) → (∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝜑))
499, 48sylbi 207 . . . . . . 7 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝜑))
506, 49impbid 202 . . . . . 6 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
51 eqeq1 2775 . . . . . . 7 (𝐴 = ⟨𝑧, 𝑤⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
5251anbi1d 615 . . . . . . . . 9 (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
53522exbidv 2004 . . . . . . . 8 (𝐴 = ⟨𝑧, 𝑤⟩ → (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
5453bibi2d 331 . . . . . . 7 (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ (𝜑 ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
5551, 54imbi12d 333 . . . . . 6 (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))) ↔ (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))))
5650, 55mpbiri 248 . . . . 5 (𝐴 = ⟨𝑧, 𝑤⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
5756adantr 466 . . . 4 ((𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
5857exlimivv 2012 . . 3 (∃𝑧𝑤(𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
593, 58sylbi 207 . 2 (𝐴 = ⟨𝑥, 𝑦⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
6059pm2.43i 52 1 (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wal 1629   = wceq 1631  wex 1852  ∃!weu 2618  cop 4322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323
This theorem is referenced by:  copsex2t  5084  copsex2g  5085  mosubopt  5103  opabid  5115  brabgaf  29751
  Copyright terms: Public domain W3C validator