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

Theorem mo4 2569
Description: At-most-one quantifier expressed using implicit substitution. This theorem is also a direct consequence of mo4f 2570, 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 2543 . . 3 (∃*𝑥𝜑 ↔ ∃𝑧𝑥(𝜑𝑥 = 𝑧))
2 mo4.1 . . . . . . . 8 (𝑥 = 𝑦 → (𝜑𝜓))
3 equequ1 2024 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
42, 3imbi12d 344 . . . . . . 7 (𝑥 = 𝑦 → ((𝜑𝑥 = 𝑧) ↔ (𝜓𝑦 = 𝑧)))
54cbvalvw 2035 . . . . . 6 (∀𝑥(𝜑𝑥 = 𝑧) ↔ ∀𝑦(𝜓𝑦 = 𝑧))
65biimpi 216 . . . . 5 (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑦(𝜓𝑦 = 𝑧))
7 pm2.27 42 . . . . . . . . . . . 12 (𝜑 → ((𝜑𝑥 = 𝑧) → 𝑥 = 𝑧))
87adantr 480 . . . . . . . . . . 11 ((𝜑𝜓) → ((𝜑𝑥 = 𝑧) → 𝑥 = 𝑧))
9 pm2.27 42 . . . . . . . . . . . 12 (𝜓 → ((𝜓𝑦 = 𝑧) → 𝑦 = 𝑧))
109adantl 481 . . . . . . . . . . 11 ((𝜑𝜓) → ((𝜓𝑦 = 𝑧) → 𝑦 = 𝑧))
118, 10anim12d 608 . . . . . . . . . 10 ((𝜑𝜓) → (((𝜑𝑥 = 𝑧) ∧ (𝜓𝑦 = 𝑧)) → (𝑥 = 𝑧𝑦 = 𝑧)))
12 equtr2 2026 . . . . . . . . . 10 ((𝑥 = 𝑧𝑦 = 𝑧) → 𝑥 = 𝑦)
1311, 12syl6com 37 . . . . . . . . 9 (((𝜑𝑥 = 𝑧) ∧ (𝜓𝑦 = 𝑧)) → ((𝜑𝜓) → 𝑥 = 𝑦))
1413ex 412 . . . . . . . 8 ((𝜑𝑥 = 𝑧) → ((𝜓𝑦 = 𝑧) → ((𝜑𝜓) → 𝑥 = 𝑦)))
1514alimdv 1915 . . . . . . 7 ((𝜑𝑥 = 𝑧) → (∀𝑦(𝜓𝑦 = 𝑧) → ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
1615com12 32 . . . . . 6 (∀𝑦(𝜓𝑦 = 𝑧) → ((𝜑𝑥 = 𝑧) → ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
1716alimdv 1915 . . . . 5 (∀𝑦(𝜓𝑦 = 𝑧) → (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
186, 17mpcom 38 . . . 4 (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
1918exlimiv 1929 . . 3 (∃𝑧𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
201, 19sylbi 217 . 2 (∃*𝑥𝜑 → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
212cbvexvw 2036 . . . . 5 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
2221biimpri 228 . . . 4 (∃𝑦𝜓 → ∃𝑥𝜑)
23 ax6evr 2014 . . . . . . . 8 𝑧 𝑥 = 𝑧
24 pm3.2 469 . . . . . . . . . . . . . . 15 (𝜑 → (𝜓 → (𝜑𝜓)))
2524imim1d 82 . . . . . . . . . . . . . 14 (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑥 = 𝑦)))
26 ax7 2015 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
2725, 26syl8 76 . . . . . . . . . . . . 13 (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓 → (𝑥 = 𝑧𝑦 = 𝑧))))
2827com4r 94 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑦 = 𝑧))))
2928impcom 407 . . . . . . . . . . 11 ((𝜑𝑥 = 𝑧) → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑦 = 𝑧)))
3029alimdv 1915 . . . . . . . . . 10 ((𝜑𝑥 = 𝑧) → (∀𝑦((𝜑𝜓) → 𝑥 = 𝑦) → ∀𝑦(𝜓𝑦 = 𝑧)))
3130impancom 451 . . . . . . . . 9 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → (𝑥 = 𝑧 → ∀𝑦(𝜓𝑦 = 𝑧)))
3231eximdv 1916 . . . . . . . 8 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → (∃𝑧 𝑥 = 𝑧 → ∃𝑧𝑦(𝜓𝑦 = 𝑧)))
3323, 32mpi 20 . . . . . . 7 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → ∃𝑧𝑦(𝜓𝑦 = 𝑧))
34 df-mo 2543 . . . . . . 7 (∃*𝑦𝜓 ↔ ∃𝑧𝑦(𝜓𝑦 = 𝑧))
3533, 34sylibr 234 . . . . . 6 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → ∃*𝑦𝜓)
3635expcom 413 . . . . 5 (∀𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (𝜑 → ∃*𝑦𝜓))
3736aleximi 1830 . . . 4 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑥∃*𝑦𝜓))
38 ax5e 1911 . . . 4 (∃𝑥∃*𝑦𝜓 → ∃*𝑦𝜓)
3922, 37, 38syl56 36 . . 3 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (∃𝑦𝜓 → ∃*𝑦𝜓))
405exbii 1846 . . . . 5 (∃𝑧𝑥(𝜑𝑥 = 𝑧) ↔ ∃𝑧𝑦(𝜓𝑦 = 𝑧))
4140, 1, 343bitr4i 303 . . . 4 (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
42 moabs 2546 . . . 4 (∃*𝑦𝜓 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
4341, 42bitri 275 . . 3 (∃*𝑥𝜑 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
4439, 43sylibr 234 . 2 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → ∃*𝑥𝜑)
4520, 44impbii 209 1 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1535  wex 1777  ∃*wmo 2541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-mo 2543
This theorem is referenced by:  eu4  2618  moel  3410  moelOLD  3413  moeq  3729  rmo4  3752  mosneq  4867  dffun6  6586  dffun3OLD  6588  fun11  6652  brprcneu  6910  brprcneuALT  6911  dff13  7292  caovmo  7687  wemoiso  8014  wemoiso2  8015  addsrmo  11142  mulsrmo  11143  summo  15765  prodmo  15984  hausflimi  24009  vitalilem3  25664  plyexmo  26373  nosupprefixmo  27763  noinfprefixmo  27764  tglineintmo  28668  ajmoi  30890  pjhthmo  31334  adjmo  31864  satfv0  35326  satfv0fun  35339  satffunlem1lem1  35370  satffunlem2lem1  35372  funtransport  35995  funray  36104  funline  36106  lineintmo  36121  cossssid4  38426  dffrege115  43940  mof0ALT  48553  mofsn  48557  f1omo  48574  thincmo  48696
  Copyright terms: Public domain W3C validator