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

Theorem copsexg 5407
Description: Substitution of class 𝐴 for ordered pair 𝑥, 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2373. Use the weaker copsexgw 5406 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.)
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 3434 . . . 4 𝑥 ∈ V
2 vex 3434 . . . 4 𝑦 ∈ V
31, 2eqvinop 5403 . . 3 (𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑧𝑤(𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
4 19.8a 2177 . . . . . . . . 9 (∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
5419.23bi 2187 . . . . . . . 8 ((⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
65ex 412 . . . . . . 7 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 → ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
7 vex 3434 . . . . . . . . 9 𝑧 ∈ V
8 vex 3434 . . . . . . . . 9 𝑤 ∈ V
97, 8opth 5393 . . . . . . . 8 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝑧 = 𝑥𝑤 = 𝑦))
109anbi1i 623 . . . . . . . . . 10 ((⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑))
11102exbii 1854 . . . . . . . . 9 (∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑))
12 nfe1 2150 . . . . . . . . . . 11 𝑥𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))
13 19.8a 2177 . . . . . . . . . . . . . . . 16 ((𝑤 = 𝑦𝜑) → ∃𝑦(𝑤 = 𝑦𝜑))
1413anim2i 616 . . . . . . . . . . . . . . 15 ((𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
1514anassrs 467 . . . . . . . . . . . . . 14 (((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
1615eximi 1840 . . . . . . . . . . . . 13 (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑦(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
17 biidd 261 . . . . . . . . . . . . . 14 (∀𝑦 𝑦 = 𝑥 → ((𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) ↔ (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
1817drex1 2442 . . . . . . . . . . . . 13 (∀𝑦 𝑦 = 𝑥 → (∃𝑦(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) ↔ ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
1916, 18syl5ib 243 . . . . . . . . . . . 12 (∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
20 anass 468 . . . . . . . . . . . . . . 15 (((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) ↔ (𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)))
2120exbii 1853 . . . . . . . . . . . . . 14 (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) ↔ ∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)))
22 19.40 1892 . . . . . . . . . . . . . . 15 (∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)) → (∃𝑦 𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
23 nfeqf2 2378 . . . . . . . . . . . . . . . . 17 (¬ ∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦 𝑧 = 𝑥)
242319.9d 2199 . . . . . . . . . . . . . . . 16 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦 𝑧 = 𝑥𝑧 = 𝑥))
2524anim1d 610 . . . . . . . . . . . . . . 15 (¬ ∀𝑦 𝑦 = 𝑥 → ((∃𝑦 𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
2622, 25syl5 34 . . . . . . . . . . . . . 14 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
2721, 26syl5bi 241 . . . . . . . . . . . . 13 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
28 19.8a 2177 . . . . . . . . . . . . 13 ((𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
2927, 28syl6 35 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
3019, 29pm2.61i 182 . . . . . . . . . . 11 (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
3112, 30exlimi 2213 . . . . . . . . . 10 (∃𝑥𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
32 euequ 2598 . . . . . . . . . . . . . 14 ∃!𝑥 𝑥 = 𝑧
33 equcom 2024 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧𝑧 = 𝑥)
3433eubii 2586 . . . . . . . . . . . . . 14 (∃!𝑥 𝑥 = 𝑧 ↔ ∃!𝑥 𝑧 = 𝑥)
3532, 34mpbi 229 . . . . . . . . . . . . 13 ∃!𝑥 𝑧 = 𝑥
36 eupick 2636 . . . . . . . . . . . . 13 ((∃!𝑥 𝑧 = 𝑥 ∧ ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))) → (𝑧 = 𝑥 → ∃𝑦(𝑤 = 𝑦𝜑)))
3735, 36mpan 686 . . . . . . . . . . . 12 (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 → ∃𝑦(𝑤 = 𝑦𝜑)))
3837com12 32 . . . . . . . . . . 11 (𝑧 = 𝑥 → (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → ∃𝑦(𝑤 = 𝑦𝜑)))
39 euequ 2598 . . . . . . . . . . . . . 14 ∃!𝑦 𝑦 = 𝑤
40 equcom 2024 . . . . . . . . . . . . . . 15 (𝑦 = 𝑤𝑤 = 𝑦)
4140eubii 2586 . . . . . . . . . . . . . 14 (∃!𝑦 𝑦 = 𝑤 ↔ ∃!𝑦 𝑤 = 𝑦)
4239, 41mpbi 229 . . . . . . . . . . . . 13 ∃!𝑦 𝑤 = 𝑦
43 eupick 2636 . . . . . . . . . . . . 13 ((∃!𝑦 𝑤 = 𝑦 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → (𝑤 = 𝑦𝜑))
4442, 43mpan 686 . . . . . . . . . . . 12 (∃𝑦(𝑤 = 𝑦𝜑) → (𝑤 = 𝑦𝜑))
4544com12 32 . . . . . . . . . . 11 (𝑤 = 𝑦 → (∃𝑦(𝑤 = 𝑦𝜑) → 𝜑))
4638, 45sylan9 507 . . . . . . . . . 10 ((𝑧 = 𝑥𝑤 = 𝑦) → (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → 𝜑))
4731, 46syl5 34 . . . . . . . . 9 ((𝑧 = 𝑥𝑤 = 𝑦) → (∃𝑥𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → 𝜑))
4811, 47syl5bi 241 . . . . . . . 8 ((𝑧 = 𝑥𝑤 = 𝑦) → (∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝜑))
499, 48sylbi 216 . . . . . . 7 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝜑))
506, 49impbid 211 . . . . . 6 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
51 eqeq1 2743 . . . . . . 7 (𝐴 = ⟨𝑧, 𝑤⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
5251anbi1d 629 . . . . . . . . 9 (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
53522exbidv 1930 . . . . . . . 8 (𝐴 = ⟨𝑧, 𝑤⟩ → (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
5453bibi2d 342 . . . . . . 7 (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ (𝜑 ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
5551, 54imbi12d 344 . . . . . 6 (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))) ↔ (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))))
5650, 55mpbiri 257 . . . . 5 (𝐴 = ⟨𝑧, 𝑤⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
5756adantr 480 . . . 4 ((𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
5857exlimivv 1938 . . 3 (∃𝑧𝑤(𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
593, 58sylbi 216 . 2 (𝐴 = ⟨𝑥, 𝑦⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
6059pm2.43i 52 1 (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wal 1539   = wceq 1541  wex 1785  ∃!weu 2569  cop 4572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-12 2174  ax-13 2373  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573
This theorem is referenced by:  opabid  5440
  Copyright terms: Public domain W3C validator