Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rmo4fOLD Structured version   Visualization version   GIF version

Theorem rmo4fOLD 29182
Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by Thierry Arnoux, 11-Oct-2016.) (Revised by Thierry Arnoux, 8-Mar-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
rmo4f.1 𝑥𝐴
rmo4f.2 𝑦𝐴
rmo4f.3 𝑥𝜓
rmo4f.4 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
rmo4fOLD (∃*𝑥(𝑥𝐴𝜑) ↔ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem rmo4fOLD
StepHypRef Expression
1 an4 864 . . . . . . . 8 (((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝜑𝜓)))
2 ancom 466 . . . . . . . . 9 ((𝑥𝐴𝑦𝐴) ↔ (𝑦𝐴𝑥𝐴))
32anbi1i 730 . . . . . . . 8 (((𝑥𝐴𝑦𝐴) ∧ (𝜑𝜓)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝜑𝜓)))
41, 3bitri 264 . . . . . . 7 (((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) ↔ ((𝑦𝐴𝑥𝐴) ∧ (𝜑𝜓)))
54imbi1i 339 . . . . . 6 ((((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ (((𝑦𝐴𝑥𝐴) ∧ (𝜑𝜓)) → 𝑥 = 𝑦))
6 impexp 462 . . . . . 6 ((((𝑦𝐴𝑥𝐴) ∧ (𝜑𝜓)) → 𝑥 = 𝑦) ↔ ((𝑦𝐴𝑥𝐴) → ((𝜑𝜓) → 𝑥 = 𝑦)))
7 impexp 462 . . . . . 6 (((𝑦𝐴𝑥𝐴) → ((𝜑𝜓) → 𝑥 = 𝑦)) ↔ (𝑦𝐴 → (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦))))
85, 6, 73bitri 286 . . . . 5 ((((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ (𝑦𝐴 → (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦))))
98albii 1744 . . . 4 (∀𝑦(((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ ∀𝑦(𝑦𝐴 → (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦))))
10 df-ral 2912 . . . 4 (∀𝑦𝐴 (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦)) ↔ ∀𝑦(𝑦𝐴 → (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦))))
11 nfcv 2761 . . . . . 6 𝑦𝑥
12 rmo4f.2 . . . . . 6 𝑦𝐴
1311, 12nfel 2773 . . . . 5 𝑦 𝑥𝐴
1413r19.21 2950 . . . 4 (∀𝑦𝐴 (𝑥𝐴 → ((𝜑𝜓) → 𝑥 = 𝑦)) ↔ (𝑥𝐴 → ∀𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
159, 10, 143bitr2i 288 . . 3 (∀𝑦(((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ (𝑥𝐴 → ∀𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
1615albii 1744 . 2 (∀𝑥𝑦(((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
17 nfv 1840 . . . . 5 𝑦𝜑
1813, 17nfan 1825 . . . 4 𝑦(𝑥𝐴𝜑)
1918mo3 2506 . . 3 (∃*𝑥(𝑥𝐴𝜑) ↔ ∀𝑥𝑦(((𝑥𝐴𝜑) ∧ [𝑦 / 𝑥](𝑥𝐴𝜑)) → 𝑥 = 𝑦))
20 nfcv 2761 . . . . . . . . 9 𝑥𝑦
21 rmo4f.1 . . . . . . . . 9 𝑥𝐴
2220, 21nfel 2773 . . . . . . . 8 𝑥 𝑦𝐴
23 rmo4f.3 . . . . . . . 8 𝑥𝜓
2422, 23nfan 1825 . . . . . . 7 𝑥(𝑦𝐴𝜓)
25 eleq1 2686 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
26 rmo4f.4 . . . . . . . 8 (𝑥 = 𝑦 → (𝜑𝜓))
2725, 26anbi12d 746 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
2824, 27sbie 2407 . . . . . 6 ([𝑦 / 𝑥](𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓))
2928anbi2i 729 . . . . 5 (((𝑥𝐴𝜑) ∧ [𝑦 / 𝑥](𝑥𝐴𝜑)) ↔ ((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)))
3029imbi1i 339 . . . 4 ((((𝑥𝐴𝜑) ∧ [𝑦 / 𝑥](𝑥𝐴𝜑)) → 𝑥 = 𝑦) ↔ (((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦))
31302albii 1745 . . 3 (∀𝑥𝑦(((𝑥𝐴𝜑) ∧ [𝑦 / 𝑥](𝑥𝐴𝜑)) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦(((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦))
3219, 31bitri 264 . 2 (∃*𝑥(𝑥𝐴𝜑) ↔ ∀𝑥𝑦(((𝑥𝐴𝜑) ∧ (𝑦𝐴𝜓)) → 𝑥 = 𝑦))
33 df-ral 2912 . 2 (∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
3416, 32, 333bitr4i 292 1 (∃*𝑥(𝑥𝐴𝜑) ↔ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1478   = wceq 1480  wnf 1705  [wsb 1877  wcel 1987  ∃*wmo 2470  wnfc 2748  wral 2907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator