Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax6e2ndALT Structured version   Visualization version   GIF version

Theorem ax6e2ndALT 44434
Description: If at least two sets exist (dtru 5432), then the same is true expressed in an alternate form similar to the form of ax6e 2376. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndVD 44412. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ax6e2ndALT (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
Distinct variable groups:   𝑥,𝑢   𝑦,𝑢   𝑥,𝑣

Proof of Theorem ax6e2ndALT
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 vex 3467 . . . . . . 7 𝑢 ∈ V
2 ax6e 2376 . . . . . . 7 𝑦 𝑦 = 𝑣
31, 2pm3.2i 469 . . . . . 6 (𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣)
4 19.42v 1949 . . . . . . 7 (∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣))
54biimpri 227 . . . . . 6 ((𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣) → ∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣))
63, 5ax-mp 5 . . . . 5 𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣)
7 isset 3476 . . . . . . 7 (𝑢 ∈ V ↔ ∃𝑥 𝑥 = 𝑢)
87anbi1i 622 . . . . . 6 ((𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (∃𝑥 𝑥 = 𝑢𝑦 = 𝑣))
98exbii 1842 . . . . 5 (∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ ∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣))
106, 9mpbi 229 . . . 4 𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣)
11 id 22 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
12 hbnae 2425 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
13 hbn1 2130 . . . . . . . . . . . 12 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦)
14 ax-5 1905 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑣 → ∀𝑥 𝑧 = 𝑣)
15 ax-5 1905 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑣 → ∀𝑧 𝑦 = 𝑣)
16 id 22 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦𝑧 = 𝑦)
17 equequ1 2020 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣))
1817a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑦𝑧 = 𝑦) → (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣)))
1916, 18ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣))
2014, 15, 19dvelimh 2443 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2111, 20syl 17 . . . . . . . . . . . . . 14 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2221idiALT 43981 . . . . . . . . . . . . 13 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2322alimi 1805 . . . . . . . . . . . 12 (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2413, 23syl 17 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2511, 24syl 17 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
26 19.41rg 44054 . . . . . . . . . 10 (∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣) → ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
2725, 26syl 17 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
2827idiALT 43981 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
2928alimi 1805 . . . . . . 7 (∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3012, 29syl 17 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3111, 30syl 17 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
32 exim 1828 . . . . 5 (∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)) → (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3331, 32syl 17 . . . 4 (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
34 pm3.35 801 . . . 4 ((∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) ∧ (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣))) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣))
3510, 33, 34sylancr 585 . . 3 (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣))
36 excomim 2152 . . 3 (∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
3735, 36syl 17 . 2 (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
3837idiALT 43981 1 (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wal 1531   = wceq 1533  wex 1773  wcel 2098  Vcvv 3463
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-13 2365  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3465
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator