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

Theorem ax6e2nd 39276
Description: If at least two sets exist (dtru 5006) , then the same is true expressed in an alternate form similar to the form of ax6e 2395. ax6e2nd 39276 is derived from ax6e2ndVD 39643. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ax6e2nd (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
Distinct variable groups:   𝑥,𝑢   𝑦,𝑢   𝑥,𝑣

Proof of Theorem ax6e2nd
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 vex 3343 . . . . . . 7 𝑢 ∈ V
2 ax6e 2395 . . . . . . 7 𝑦 𝑦 = 𝑣
31, 2pm3.2i 470 . . . . . 6 (𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣)
4 19.42v 2030 . . . . . . 7 (∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣))
54biimpri 218 . . . . . 6 ((𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣) → ∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣))
63, 5ax-mp 5 . . . . 5 𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣)
7 isset 3347 . . . . . . 7 (𝑢 ∈ V ↔ ∃𝑥 𝑥 = 𝑢)
87anbi1i 733 . . . . . 6 ((𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (∃𝑥 𝑥 = 𝑢𝑦 = 𝑣))
98exbii 1923 . . . . 5 (∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ ∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣))
106, 9mpbi 220 . . . 4 𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣)
11 id 22 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
12 hbnae 2459 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
13 hbn1 2169 . . . . . . . . . . . 12 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦)
14 ax-5 1988 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑣 → ∀𝑥 𝑧 = 𝑣)
15 ax-5 1988 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑣 → ∀𝑧 𝑦 = 𝑣)
16 id 22 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦𝑧 = 𝑦)
17 equequ1 2107 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣))
1816, 17syl 17 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣))
1918idiALT 39185 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣))
2014, 15, 19dvelimh 2476 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2111, 20syl 17 . . . . . . . . . . . . . 14 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2221idiALT 39185 . . . . . . . . . . . . 13 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2322alimi 1888 . . . . . . . . . . . 12 (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2413, 23syl 17 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2511, 24syl 17 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
26 19.41rg 39268 . . . . . . . . . 10 (∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣) → ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
2725, 26syl 17 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
2827idiALT 39185 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
2928alimi 1888 . . . . . . 7 (∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3012, 29syl 17 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3111, 30syl 17 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
32 exim 1910 . . . . 5 (∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)) → (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3331, 32syl 17 . . . 4 (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
34 pm2.27 42 . . . 4 (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ((∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3510, 33, 34mpsyl 68 . . 3 (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣))
36 excomim 2192 . . 3 (∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
3735, 36syl 17 . 2 (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
3837idiALT 39185 1 (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  wal 1630  wex 1853  wcel 2139  Vcvv 3340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-v 3342
This theorem is referenced by:  ax6e2ndeq  39277  ax6e2ndeqVD  39644  ax6e2ndeqALT  39666
  Copyright terms: Public domain W3C validator