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

Theorem rmo4 3727
Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by NM, 16-Jun-2017.)
Hypothesis
Ref Expression
rmo4.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
rmo4 (∃*𝑥𝐴 𝜑 ↔ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem rmo4
StepHypRef Expression
1 df-rmo 3377 . 2 (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
2 an4 655 . . . . . . . . 9 (((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝜑𝜓)))
3 ancom 462 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐴) ↔ (𝑦𝐴𝑥𝐴))
43anbi1i 625 . . . . . . . . 9 (((𝑥𝐴𝑦𝐴) ∧ (𝜑𝜓)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝜑𝜓)))
52, 4bitri 275 . . . . . . . 8 (((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝜑𝜓)))
65imbi1i 350 . . . . . . 7 ((((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ (((𝑦𝐴𝑥𝐴) ∧ (𝜑𝜓)) → 𝑥 = 𝑦))
7 impexp 452 . . . . . . 7 ((((𝑦𝐴𝑥𝐴) ∧ (𝜑𝜓)) → 𝑥 = 𝑦) ↔ ((𝑦𝐴𝑥𝐴) → ((𝜑𝜓) → 𝑥 = 𝑦)))
8 impexp 452 . . . . . . 7 (((𝑦𝐴𝑥𝐴) → ((𝜑𝜓) → 𝑥 = 𝑦)) ↔ (𝑦𝐴 → (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦))))
96, 7, 83bitri 297 . . . . . 6 ((((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ (𝑦𝐴 → (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦))))
109albii 1822 . . . . 5 (∀𝑦(((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ ∀𝑦(𝑦𝐴 → (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦))))
11 df-ral 3063 . . . . 5 (∀𝑦𝐴 (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦)) ↔ ∀𝑦(𝑦𝐴 → (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦))))
12 r19.21v 3180 . . . . 5 (∀𝑦𝐴 (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦)) ↔ (𝑥𝐴 → ∀𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
1310, 11, 123bitr2i 299 . . . 4 (∀𝑦(((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ (𝑥𝐴 → ∀𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
1413albii 1822 . . 3 (∀𝑥𝑦(((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
15 eleq1w 2817 . . . . 5 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
16 rmo4.1 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
1715, 16anbi12d 632 . . . 4 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
1817mo4 2561 . . 3 (∃*𝑥(𝑥𝐴𝜑) ↔ ∀𝑥𝑦(((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦))
19 df-ral 3063 . . 3 (∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
2014, 18, 193bitr4i 303 . 2 (∃*𝑥(𝑥𝐴𝜑) ↔ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦))
211, 20bitri 275 1 (∃*𝑥𝐴 𝜑 ↔ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wal 1540  wcel 2107  ∃*wmo 2533  wral 3062  ∃*wrmo 3376
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 1914  ax-6 1972  ax-7 2012  ax-8 2109
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-mo 2535  df-clel 2811  df-ral 3063  df-rmo 3377
This theorem is referenced by:  reu4  3728  disjor  5129  somo  5626  nnasmo  8662  supmo  9447  infmo  9490  sqrmo  15198  catideu  17619  poslubmo  18364  posglbmo  18365  mgmidmo  18579  mndinvmod  18655  lspextmo  20667  evlseu  21646  ply1divmo  25653  2sqmo  26940  divsmo  27634  tghilberti2  27889  foot  27973  mideu  27989  cvmliftmo  34275  hilbert1.2  35127  poimirlem1  36489  poimirlem13  36501  poimirlem14  36502  poimirlem18  36506  poimirlem21  36509  inecmo  37224  idomsubgmo  41940
  Copyright terms: Public domain W3C validator