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

Theorem dfmoeu 2535
Description: An elementary proof of moeu 2582 in disguise, connecting an expression characterizing uniqueness (df-mo 2539) to that of existential uniqueness (eu6 2573). No particular order of definition is required, as one can be derived from the other. This is shown here and in dfeumo 2536. (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 1780 . . . . 5 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2 pm2.21 123 . . . . . 6 𝜑 → (𝜑𝑥 = 𝑦))
32alimi 1810 . . . . 5 (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑𝑥 = 𝑦))
41, 3sylbir 235 . . . 4 (¬ ∃𝑥𝜑 → ∀𝑥(𝜑𝑥 = 𝑦))
5419.8ad 2181 . . 3 (¬ ∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))
6 biimp 215 . . . . 5 ((𝜑𝑥 = 𝑦) → (𝜑𝑥 = 𝑦))
76alimi 1810 . . . 4 (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦))
87eximi 1834 . . 3 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑦𝑥(𝜑𝑥 = 𝑦))
95, 8ja 186 . 2 ((∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)) → ∃𝑦𝑥(𝜑𝑥 = 𝑦))
10 nfia1 2152 . . . . 5 𝑥(∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦))
11 id 22 . . . . . . . . 9 (𝜑𝜑)
12 ax12v 2177 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
1312com12 32 . . . . . . . . 9 (𝜑 → (𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦𝜑)))
1411, 13embantd 59 . . . . . . . 8 (𝜑 → ((𝜑𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦𝜑)))
1514spsd 2186 . . . . . . 7 (𝜑 → (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦𝜑)))
1615ancld 550 . . . . . 6 (𝜑 → (∀𝑥(𝜑𝑥 = 𝑦) → (∀𝑥(𝜑𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦𝜑))))
17 albiim 1888 . . . . . 6 (∀𝑥(𝜑𝑥 = 𝑦) ↔ (∀𝑥(𝜑𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦𝜑)))
1816, 17imbitrrdi 252 . . . . 5 (𝜑 → (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦)))
1910, 18exlimi 2216 . . . 4 (∃𝑥𝜑 → (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦)))
2019eximdv 1916 . . 3 (∃𝑥𝜑 → (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
2120com12 32 . 2 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
229, 21impbii 209 1 ((∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wal 1537  wex 1778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-10 2140  ax-12 2176
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-nf 1783
This theorem is referenced by:  dfeumo  2536  eu6  2573  dfmo  2595
  Copyright terms: Public domain W3C validator