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 39480
Description: If at least two sets exist (dtru 4887) , then the same is true expressed in an alternate form similar to the form of ax6e 2286. 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 39458. (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 3234 . . . . . . 7 𝑢 ∈ V
2 ax6e 2286 . . . . . . 7 𝑦 𝑦 = 𝑣
31, 2pm3.2i 470 . . . . . 6 (𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣)
4 19.42v 1921 . . . . . . 7 (∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣))
54biimpri 218 . . . . . 6 ((𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣) → ∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣))
63, 5ax-mp 5 . . . . 5 𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣)
7 isset 3238 . . . . . . 7 (𝑢 ∈ V ↔ ∃𝑥 𝑥 = 𝑢)
87anbi1i 731 . . . . . 6 ((𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (∃𝑥 𝑥 = 𝑢𝑦 = 𝑣))
98exbii 1814 . . . . 5 (∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ ∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣))
106, 9mpbi 220 . . . 4 𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣)
11 id 22 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
12 hbnae 2350 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
13 hbn1 2060 . . . . . . . . . . . 12 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦)
14 ax-5 1879 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑣 → ∀𝑥 𝑧 = 𝑣)
15 ax-5 1879 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑣 → ∀𝑧 𝑦 = 𝑣)
16 id 22 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦𝑧 = 𝑦)
17 equequ1 1998 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣))
1817a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑦𝑧 = 𝑦) → (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣)))
1916, 18ax-mp 5 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣))
2014, 15, 19dvelimh 2367 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2111, 20syl 17 . . . . . . . . . . . . . 14 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2221idiALT 39000 . . . . . . . . . . . . 13 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2322alimi 1779 . . . . . . . . . . . 12 (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2413, 23syl 17 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2511, 24syl 17 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
26 19.41rg 39083 . . . . . . . . . 10 (∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣) → ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
2725, 26syl 17 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
2827idiALT 39000 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
2928alimi 1779 . . . . . . 7 (∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3012, 29syl 17 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3111, 30syl 17 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
32 exim 1801 . . . . 5 (∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)) → (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3331, 32syl 17 . . . 4 (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
34 pm3.35 610 . . . 4 ((∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) ∧ (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣))) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣))
3510, 33, 34sylancr 696 . . 3 (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣))
36 excomim 2083 . . 3 (∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
3735, 36syl 17 . 2 (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
3837idiALT 39000 1 (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  wal 1521   = wceq 1523  wex 1744  wcel 2030  Vcvv 3231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator