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

Theorem mo4 2584
 Description: At-most-one quantifier expressed using implicit substitution. This theorem is also a direct consequence of mo4f 2585, but this proof is based on fewer axioms. By the way, swapping 𝑥, 𝑦 and 𝜑, 𝜓 leads to an expression for ∃*𝑦𝜓, which is equivalent to ∃*𝑥𝜑 (is a proof line), so the right hand side is a rare instance of an expression where swapping the quantifiers can be done without ax-11 2158. (Contributed by NM, 26-Jul-1995.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2023.)
Hypothesis
Ref Expression
mo4.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
mo4 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem mo4
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-mo 2557 . . 3 (∃*𝑥𝜑 ↔ ∃𝑧𝑥(𝜑𝑥 = 𝑧))
2 mo4.1 . . . . . . . 8 (𝑥 = 𝑦 → (𝜑𝜓))
3 equequ1 2032 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
42, 3imbi12d 348 . . . . . . 7 (𝑥 = 𝑦 → ((𝜑𝑥 = 𝑧) ↔ (𝜓𝑦 = 𝑧)))
54cbvalvw 2043 . . . . . 6 (∀𝑥(𝜑𝑥 = 𝑧) ↔ ∀𝑦(𝜓𝑦 = 𝑧))
65biimpi 219 . . . . 5 (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑦(𝜓𝑦 = 𝑧))
7 pm2.27 42 . . . . . . . . . . . 12 (𝜑 → ((𝜑𝑥 = 𝑧) → 𝑥 = 𝑧))
87adantr 484 . . . . . . . . . . 11 ((𝜑𝜓) → ((𝜑𝑥 = 𝑧) → 𝑥 = 𝑧))
9 pm2.27 42 . . . . . . . . . . . 12 (𝜓 → ((𝜓𝑦 = 𝑧) → 𝑦 = 𝑧))
109adantl 485 . . . . . . . . . . 11 ((𝜑𝜓) → ((𝜓𝑦 = 𝑧) → 𝑦 = 𝑧))
118, 10anim12d 611 . . . . . . . . . 10 ((𝜑𝜓) → (((𝜑𝑥 = 𝑧) ∧ (𝜓𝑦 = 𝑧)) → (𝑥 = 𝑧𝑦 = 𝑧)))
12 equtr2 2034 . . . . . . . . . 10 ((𝑥 = 𝑧𝑦 = 𝑧) → 𝑥 = 𝑦)
1311, 12syl6com 37 . . . . . . . . 9 (((𝜑𝑥 = 𝑧) ∧ (𝜓𝑦 = 𝑧)) → ((𝜑𝜓) → 𝑥 = 𝑦))
1413ex 416 . . . . . . . 8 ((𝜑𝑥 = 𝑧) → ((𝜓𝑦 = 𝑧) → ((𝜑𝜓) → 𝑥 = 𝑦)))
1514alimdv 1917 . . . . . . 7 ((𝜑𝑥 = 𝑧) → (∀𝑦(𝜓𝑦 = 𝑧) → ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
1615com12 32 . . . . . 6 (∀𝑦(𝜓𝑦 = 𝑧) → ((𝜑𝑥 = 𝑧) → ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
1716alimdv 1917 . . . . 5 (∀𝑦(𝜓𝑦 = 𝑧) → (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
186, 17mpcom 38 . . . 4 (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
1918exlimiv 1931 . . 3 (∃𝑧𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
201, 19sylbi 220 . 2 (∃*𝑥𝜑 → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
212cbvexvw 2044 . . . . 5 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
2221biimpri 231 . . . 4 (∃𝑦𝜓 → ∃𝑥𝜑)
23 ax6evr 2022 . . . . . . . 8 𝑧 𝑥 = 𝑧
24 pm3.2 473 . . . . . . . . . . . . . . 15 (𝜑 → (𝜓 → (𝜑𝜓)))
2524imim1d 82 . . . . . . . . . . . . . 14 (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑥 = 𝑦)))
26 ax7 2023 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
2725, 26syl8 76 . . . . . . . . . . . . 13 (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓 → (𝑥 = 𝑧𝑦 = 𝑧))))
2827com4r 94 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑦 = 𝑧))))
2928impcom 411 . . . . . . . . . . 11 ((𝜑𝑥 = 𝑧) → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑦 = 𝑧)))
3029alimdv 1917 . . . . . . . . . 10 ((𝜑𝑥 = 𝑧) → (∀𝑦((𝜑𝜓) → 𝑥 = 𝑦) → ∀𝑦(𝜓𝑦 = 𝑧)))
3130impancom 455 . . . . . . . . 9 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → (𝑥 = 𝑧 → ∀𝑦(𝜓𝑦 = 𝑧)))
3231eximdv 1918 . . . . . . . 8 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → (∃𝑧 𝑥 = 𝑧 → ∃𝑧𝑦(𝜓𝑦 = 𝑧)))
3323, 32mpi 20 . . . . . . 7 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → ∃𝑧𝑦(𝜓𝑦 = 𝑧))
34 df-mo 2557 . . . . . . 7 (∃*𝑦𝜓 ↔ ∃𝑧𝑦(𝜓𝑦 = 𝑧))
3533, 34sylibr 237 . . . . . 6 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → ∃*𝑦𝜓)
3635expcom 417 . . . . 5 (∀𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (𝜑 → ∃*𝑦𝜓))
3736aleximi 1833 . . . 4 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑥∃*𝑦𝜓))
38 ax5e 1913 . . . 4 (∃𝑥∃*𝑦𝜓 → ∃*𝑦𝜓)
3922, 37, 38syl56 36 . . 3 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (∃𝑦𝜓 → ∃*𝑦𝜓))
405exbii 1849 . . . . 5 (∃𝑧𝑥(𝜑𝑥 = 𝑧) ↔ ∃𝑧𝑦(𝜓𝑦 = 𝑧))
4140, 1, 343bitr4i 306 . . . 4 (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
42 moabs 2560 . . . 4 (∃*𝑦𝜓 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
4341, 42bitri 278 . . 3 (∃*𝑥𝜑 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
4439, 43sylibr 237 . 2 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → ∃*𝑥𝜑)
4520, 44impbii 212 1 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536  ∃wex 1781  ∃*wmo 2555 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-mo 2557 This theorem is referenced by:  eu4  2635  moeq  3623  rmo4  3646  mosneq  4733  dffun3  6351  fun11  6414  brprcneu  6654  fvprc  6655  dff13  7011  mpofunOLD  7277  caovmo  7387  wemoiso  7684  wemoiso2  7685  addsrmo  10546  mulsrmo  10547  summo  15135  prodmo  15351  hausflimi  22693  vitalilem3  24323  plyexmo  25021  tglineintmo  26548  ajmoi  28753  pjhthmo  29197  adjmo  29727  moel  30371  satfv0  32848  satfv0fun  32861  satffunlem1lem1  32892  satffunlem2lem1  32894  nosupprefixmo  33500  noinfprefixmo  33501  funtransport  33916  funray  34025  funline  34027  lineintmo  34042  cossssid4  36184  dffrege115  41087
 Copyright terms: Public domain W3C validator