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

Theorem dfmoeu 2554
 Description: An elementary proof of moeu 2603 in disguise, connecting an expression characterizing uniqueness (df-mo 2558) to that of existential uniqueness (eu6 2594). No particular order of definition is required, as one can be derived from the other. This is shown here and in dfeumo 2555. (Contributed by Wolf Lammen, 27-May-2019.)
Assertion
Ref Expression
dfmoeu ((∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem dfmoeu
StepHypRef Expression
1 alnex 1784 . . . . 5 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2 pm2.21 123 . . . . . 6 𝜑 → (𝜑𝑥 = 𝑦))
32alimi 1814 . . . . 5 (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑𝑥 = 𝑦))
41, 3sylbir 238 . . . 4 (¬ ∃𝑥𝜑 → ∀𝑥(𝜑𝑥 = 𝑦))
5419.8ad 2180 . . 3 (¬ ∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))
6 biimp 218 . . . . 5 ((𝜑𝑥 = 𝑦) → (𝜑𝑥 = 𝑦))
76alimi 1814 . . . 4 (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦))
87eximi 1837 . . 3 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑦𝑥(𝜑𝑥 = 𝑦))
95, 8ja 189 . 2 ((∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)) → ∃𝑦𝑥(𝜑𝑥 = 𝑦))
10 nfia1 2155 . . . . 5 𝑥(∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦))
11 id 22 . . . . . . . . 9 (𝜑𝜑)
12 ax12v 2177 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
1312com12 32 . . . . . . . . 9 (𝜑 → (𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦𝜑)))
1411, 13embantd 59 . . . . . . . 8 (𝜑 → ((𝜑𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦𝜑)))
1514spsd 2185 . . . . . . 7 (𝜑 → (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦𝜑)))
1615ancld 555 . . . . . 6 (𝜑 → (∀𝑥(𝜑𝑥 = 𝑦) → (∀𝑥(𝜑𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦𝜑))))
17 albiim 1891 . . . . . 6 (∀𝑥(𝜑𝑥 = 𝑦) ↔ (∀𝑥(𝜑𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦𝜑)))
1816, 17syl6ibr 255 . . . . 5 (𝜑 → (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦)))
1910, 18exlimi 2216 . . . 4 (∃𝑥𝜑 → (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦)))
2019eximdv 1919 . . 3 (∃𝑥𝜑 → (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
2120com12 32 . 2 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
229, 21impbii 212 1 ((∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1537  ∃wex 1782 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-10 2143  ax-12 2176 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-ex 1783  df-nf 1787 This theorem is referenced by:  dfeumo  2555  eu6  2594  dfmo  2617
 Copyright terms: Public domain W3C validator