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

Theorem dfmoeu 2615
Description: An elementary proof of moeu 2665 in disguise, connecting an expression characterizing uniqueness (df-mo 2619) to that of existential uniqueness (eu6 2656). No particular order of definition is required, as one can be derived from the other. This is shown here and in dfeumo 2616. (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 1775 . . . . 5 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2 pm2.21 123 . . . . . 6 𝜑 → (𝜑𝑥 = 𝑦))
32alimi 1805 . . . . 5 (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑𝑥 = 𝑦))
41, 3sylbir 236 . . . 4 (¬ ∃𝑥𝜑 → ∀𝑥(𝜑𝑥 = 𝑦))
5419.8ad 2173 . . 3 (¬ ∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))
6 biimp 216 . . . . 5 ((𝜑𝑥 = 𝑦) → (𝜑𝑥 = 𝑦))
76alimi 1805 . . . 4 (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦))
87eximi 1828 . . 3 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑦𝑥(𝜑𝑥 = 𝑦))
95, 8ja 187 . 2 ((∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)) → ∃𝑦𝑥(𝜑𝑥 = 𝑦))
10 nfia1 2150 . . . . 5 𝑥(∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦))
11 id 22 . . . . . . . . 9 (𝜑𝜑)
12 ax12v 2170 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
1312com12 32 . . . . . . . . 9 (𝜑 → (𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦𝜑)))
1411, 13embantd 59 . . . . . . . 8 (𝜑 → ((𝜑𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦𝜑)))
1514spsd 2178 . . . . . . 7 (𝜑 → (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦𝜑)))
1615ancld 551 . . . . . 6 (𝜑 → (∀𝑥(𝜑𝑥 = 𝑦) → (∀𝑥(𝜑𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦𝜑))))
17 albiim 1883 . . . . . 6 (∀𝑥(𝜑𝑥 = 𝑦) ↔ (∀𝑥(𝜑𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦𝜑)))
1816, 17syl6ibr 253 . . . . 5 (𝜑 → (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦)))
1910, 18exlimi 2210 . . . 4 (∃𝑥𝜑 → (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦)))
2019eximdv 1911 . . 3 (∃𝑥𝜑 → (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
2120com12 32 . 2 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
229, 21impbii 210 1 ((∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wal 1528  wex 1773
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 1904  ax-6 1963  ax-7 2008  ax-10 2138  ax-12 2169
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-ex 1774  df-nf 1778
This theorem is referenced by:  dfeumo  2616  eu6  2656  dfmo  2679
  Copyright terms: Public domain W3C validator