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

Theorem copsexg 4728
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 3069 . . . 4 𝑥 ∈ V
2 vex 3069 . . . 4 𝑦 ∈ V
31, 2eqvinop 4727 . . 3 (𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑧𝑤(𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
4 19.8a 1988 . . . . . . . . 9 (∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
5419.23bi 2002 . . . . . . . 8 ((⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
65ex 443 . . . . . . 7 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 → ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
7 vex 3069 . . . . . . . . 9 𝑧 ∈ V
8 vex 3069 . . . . . . . . 9 𝑤 ∈ V
97, 8opth 4717 . . . . . . . 8 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝑧 = 𝑥𝑤 = 𝑦))
109anbi1i 718 . . . . . . . . . 10 ((⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑))
11102exbii 1750 . . . . . . . . 9 (∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑))
12 nfe1 1968 . . . . . . . . . . 11 𝑥𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))
13 19.8a 1988 . . . . . . . . . . . . . . . 16 ((𝑤 = 𝑦𝜑) → ∃𝑦(𝑤 = 𝑦𝜑))
1413anim2i 585 . . . . . . . . . . . . . . 15 ((𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
1514anassrs 669 . . . . . . . . . . . . . 14 (((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
1615eximi 1738 . . . . . . . . . . . . 13 (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑦(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
17 biidd 247 . . . . . . . . . . . . . 14 (∀𝑦 𝑦 = 𝑥 → ((𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) ↔ (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
1817drex1 2210 . . . . . . . . . . . . 13 (∀𝑦 𝑦 = 𝑥 → (∃𝑦(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) ↔ ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
1916, 18syl5ib 229 . . . . . . . . . . . 12 (∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
20 anass 670 . . . . . . . . . . . . . . 15 (((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) ↔ (𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)))
2120exbii 1749 . . . . . . . . . . . . . 14 (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) ↔ ∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)))
22 19.40 1762 . . . . . . . . . . . . . . 15 (∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)) → (∃𝑦 𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
23 nfeqf2 2182 . . . . . . . . . . . . . . . . 17 (¬ ∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦 𝑧 = 𝑥)
242319.9d 2021 . . . . . . . . . . . . . . . 16 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦 𝑧 = 𝑥𝑧 = 𝑥))
2524anim1d 580 . . . . . . . . . . . . . . 15 (¬ ∀𝑦 𝑦 = 𝑥 → ((∃𝑦 𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
2622, 25syl5 33 . . . . . . . . . . . . . 14 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
2721, 26syl5bi 227 . . . . . . . . . . . . 13 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
28 19.8a 1988 . . . . . . . . . . . . 13 ((𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
2927, 28syl6 34 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
3019, 29pm2.61i 171 . . . . . . . . . . 11 (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
3112, 30exlimi 2048 . . . . . . . . . 10 (∃𝑥𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
32 euequ1 2359 . . . . . . . . . . . . . 14 ∃!𝑥 𝑥 = 𝑧
33 equcom 1894 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧𝑧 = 𝑥)
3433eubii 2375 . . . . . . . . . . . . . 14 (∃!𝑥 𝑥 = 𝑧 ↔ ∃!𝑥 𝑧 = 𝑥)
3532, 34mpbi 215 . . . . . . . . . . . . 13 ∃!𝑥 𝑧 = 𝑥
36 eupick 2419 . . . . . . . . . . . . 13 ((∃!𝑥 𝑧 = 𝑥 ∧ ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))) → (𝑧 = 𝑥 → ∃𝑦(𝑤 = 𝑦𝜑)))
3735, 36mpan 693 . . . . . . . . . . . 12 (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 → ∃𝑦(𝑤 = 𝑦𝜑)))
3837com12 32 . . . . . . . . . . 11 (𝑧 = 𝑥 → (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → ∃𝑦(𝑤 = 𝑦𝜑)))
39 euequ1 2359 . . . . . . . . . . . . . 14 ∃!𝑦 𝑦 = 𝑤
40 equcom 1894 . . . . . . . . . . . . . . 15 (𝑦 = 𝑤𝑤 = 𝑦)
4140eubii 2375 . . . . . . . . . . . . . 14 (∃!𝑦 𝑦 = 𝑤 ↔ ∃!𝑦 𝑤 = 𝑦)
4239, 41mpbi 215 . . . . . . . . . . . . 13 ∃!𝑦 𝑤 = 𝑦
43 eupick 2419 . . . . . . . . . . . . 13 ((∃!𝑦 𝑤 = 𝑦 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → (𝑤 = 𝑦𝜑))
4442, 43mpan 693 . . . . . . . . . . . 12 (∃𝑦(𝑤 = 𝑦𝜑) → (𝑤 = 𝑦𝜑))
4544com12 32 . . . . . . . . . . 11 (𝑤 = 𝑦 → (∃𝑦(𝑤 = 𝑦𝜑) → 𝜑))
4638, 45sylan9 678 . . . . . . . . . 10 ((𝑧 = 𝑥𝑤 = 𝑦) → (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → 𝜑))
4731, 46syl5 33 . . . . . . . . 9 ((𝑧 = 𝑥𝑤 = 𝑦) → (∃𝑥𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → 𝜑))
4811, 47syl5bi 227 . . . . . . . 8 ((𝑧 = 𝑥𝑤 = 𝑦) → (∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝜑))
499, 48sylbi 202 . . . . . . 7 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝜑))
506, 49impbid 197 . . . . . 6 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
51 eqeq1 2509 . . . . . . 7 (𝐴 = ⟨𝑧, 𝑤⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
5251anbi1d 728 . . . . . . . . 9 (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
53522exbidv 1801 . . . . . . . 8 (𝐴 = ⟨𝑧, 𝑤⟩ → (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
5453bibi2d 327 . . . . . . 7 (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ (𝜑 ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
5551, 54imbi12d 329 . . . . . 6 (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))) ↔ (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))))
5650, 55mpbiri 243 . . . . 5 (𝐴 = ⟨𝑧, 𝑤⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
5756adantr 474 . . . 4 ((𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
5857exlimivv 1809 . . 3 (∃𝑧𝑤(𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
593, 58sylbi 202 . 2 (𝐴 = ⟨𝑥, 𝑦⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
6059pm2.43i 49 1 (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 191  wa 378  wal 1466   = wceq 1468  wex 1692  ∃!weu 2353  cop 4001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pr 4680
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002
This theorem is referenced by:  copsex2t  4729  copsex2g  4730  mosubopt  4740  opabid  4749  brabgaf  28374
  Copyright terms: Public domain W3C validator