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

Theorem rmo4 3532
 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 3050 . 2 (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
2 an4 900 . . . . . . . . 9 (((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝜑𝜓)))
3 ancom 465 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐴) ↔ (𝑦𝐴𝑥𝐴))
43anbi1i 733 . . . . . . . . 9 (((𝑥𝐴𝑦𝐴) ∧ (𝜑𝜓)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝜑𝜓)))
52, 4bitri 264 . . . . . . . 8 (((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝜑𝜓)))
65imbi1i 338 . . . . . . 7 ((((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ (((𝑦𝐴𝑥𝐴) ∧ (𝜑𝜓)) → 𝑥 = 𝑦))
7 impexp 461 . . . . . . 7 ((((𝑦𝐴𝑥𝐴) ∧ (𝜑𝜓)) → 𝑥 = 𝑦) ↔ ((𝑦𝐴𝑥𝐴) → ((𝜑𝜓) → 𝑥 = 𝑦)))
8 impexp 461 . . . . . . 7 (((𝑦𝐴𝑥𝐴) → ((𝜑𝜓) → 𝑥 = 𝑦)) ↔ (𝑦𝐴 → (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦))))
96, 7, 83bitri 286 . . . . . 6 ((((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ (𝑦𝐴 → (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦))))
109albii 1888 . . . . 5 (∀𝑦(((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ ∀𝑦(𝑦𝐴 → (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦))))
11 df-ral 3047 . . . . 5 (∀𝑦𝐴 (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦)) ↔ ∀𝑦(𝑦𝐴 → (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦))))
12 r19.21v 3090 . . . . 5 (∀𝑦𝐴 (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦)) ↔ (𝑥𝐴 → ∀𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
1310, 11, 123bitr2i 288 . . . 4 (∀𝑦(((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ (𝑥𝐴 → ∀𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
1413albii 1888 . . 3 (∀𝑥𝑦(((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
15 eleq1w 2814 . . . . 5 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
16 rmo4.1 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
1715, 16anbi12d 749 . . . 4 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
1817mo4 2647 . . 3 (∃*𝑥(𝑥𝐴𝜑) ↔ ∀𝑥𝑦(((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦))
19 df-ral 3047 . . 3 (∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
2014, 18, 193bitr4i 292 . 2 (∃*𝑥(𝑥𝐴𝜑) ↔ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦))
211, 20bitri 264 1 (∃*𝑥𝐴 𝜑 ↔ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1622   ∈ wcel 2131  ∃*wmo 2600  ∀wral 3042  ∃*wrmo 3045 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clel 2748  df-ral 3047  df-rmo 3050 This theorem is referenced by:  reu4  3533  disjor  4778  somo  5213  supmo  8515  infmo  8558  sqrmo  14183  catideu  16529  poslubmo  17339  posglbmo  17340  mgmidmo  17452  lspextmo  19250  evlseu  19710  ply1divmo  24086  tghilberti2  25724  foot  25805  mideu  25821  2sqmo  29950  cvmliftmo  31565  hilbert1.2  32560  poimirlem1  33715  poimirlem13  33727  poimirlem14  33728  poimirlem18  33732  poimirlem21  33735  inecmo  34435  idomsubgmo  38270
 Copyright terms: Public domain W3C validator