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

Theorem mo4f 2654
 Description: "At most one" expressed using implicit substitution. (Contributed by NM, 10-Apr-2004.)
Hypotheses
Ref Expression
mo4f.1 𝑥𝜓
mo4f.2 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
mo4f (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥,𝑦)

Proof of Theorem mo4f
StepHypRef Expression
1 nfv 1992 . . 3 𝑦𝜑
21mo3 2645 . 2 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
3 mo4f.1 . . . . . 6 𝑥𝜓
4 mo4f.2 . . . . . 6 (𝑥 = 𝑦 → (𝜑𝜓))
53, 4sbie 2545 . . . . 5 ([𝑦 / 𝑥]𝜑𝜓)
65anbi2i 732 . . . 4 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝜑𝜓))
76imbi1i 338 . . 3 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ((𝜑𝜓) → 𝑥 = 𝑦))
872albii 1897 . 2 (∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
92, 8bitri 264 1 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1630  Ⅎwnf 1857  [wsb 2046  ∃*wmo 2608 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612 This theorem is referenced by:  mo4  2655  bm1.1  2745  mob2  3527  moop2  5114
 Copyright terms: Public domain W3C validator