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 39977
Description: If at least two sets exist (dtru 5070) , then the same is true expressed in an alternate form similar to the form of ax6e 2402. 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 39955. (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 3417 . . . . . . 7 𝑢 ∈ V
2 ax6e 2402 . . . . . . 7 𝑦 𝑦 = 𝑣
31, 2pm3.2i 464 . . . . . 6 (𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣)
4 19.42v 2052 . . . . . . 7 (∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣))
54biimpri 220 . . . . . 6 ((𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣) → ∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣))
63, 5ax-mp 5 . . . . 5 𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣)
7 isset 3424 . . . . . . 7 (𝑢 ∈ V ↔ ∃𝑥 𝑥 = 𝑢)
87anbi1i 617 . . . . . 6 ((𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (∃𝑥 𝑥 = 𝑢𝑦 = 𝑣))
98exbii 1947 . . . . 5 (∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ ∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣))
106, 9mpbi 222 . . . 4 𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣)
11 id 22 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
12 hbnae 2454 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
13 hbn1 2193 . . . . . . . . . . . 12 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦)
14 ax-5 2009 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑣 → ∀𝑥 𝑧 = 𝑣)
15 ax-5 2009 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑣 → ∀𝑧 𝑦 = 𝑣)
16 id 22 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦𝑧 = 𝑦)
17 equequ1 2129 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣))
1817a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑦𝑧 = 𝑦) → (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣)))
1916, 18ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣))
2014, 15, 19dvelimh 2471 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2111, 20syl 17 . . . . . . . . . . . . . 14 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2221idiALT 39514 . . . . . . . . . . . . 13 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2322alimi 1910 . . . . . . . . . . . 12 (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2413, 23syl 17 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2511, 24syl 17 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
26 19.41rg 39587 . . . . . . . . . 10 (∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣) → ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
2725, 26syl 17 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
2827idiALT 39514 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
2928alimi 1910 . . . . . . 7 (∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3012, 29syl 17 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3111, 30syl 17 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
32 exim 1932 . . . . 5 (∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)) → (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3331, 32syl 17 . . . 4 (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
34 pm3.35 837 . . . 4 ((∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) ∧ (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣))) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣))
3510, 33, 34sylancr 581 . . 3 (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣))
36 excomim 2213 . . 3 (∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
3735, 36syl 17 . 2 (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
3837idiALT 39514 1 (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wal 1654   = wceq 1656  wex 1878  wcel 2164  Vcvv 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-v 3416
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator