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

Theorem moel 3357
Description: "At most one" element in a set. (Contributed by Thierry Arnoux, 26-Jul-2018.) Avoid ax-11 2154. (Revised by Wolf Lammen, 23-Nov-2024.)
Assertion
Ref Expression
moel (∃*𝑥 𝑥𝐴 ↔ ∀𝑥𝐴𝑦𝐴 𝑥 = 𝑦)
Distinct variable group:   𝑥,𝑦,𝐴

Proof of Theorem moel
StepHypRef Expression
1 19.21v 1942 . . . 4 (∀𝑦(𝑥𝐴 → (𝑦𝐴𝑥 = 𝑦)) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝐴𝑥 = 𝑦)))
2 impexp 451 . . . . 5 (((𝑥𝐴𝑦𝐴) → 𝑥 = 𝑦) ↔ (𝑥𝐴 → (𝑦𝐴𝑥 = 𝑦)))
32albii 1822 . . . 4 (∀𝑦((𝑥𝐴𝑦𝐴) → 𝑥 = 𝑦) ↔ ∀𝑦(𝑥𝐴 → (𝑦𝐴𝑥 = 𝑦)))
4 df-ral 3069 . . . . 5 (∀𝑦𝐴 𝑥 = 𝑦 ↔ ∀𝑦(𝑦𝐴𝑥 = 𝑦))
54imbi2i 336 . . . 4 ((𝑥𝐴 → ∀𝑦𝐴 𝑥 = 𝑦) ↔ (𝑥𝐴 → ∀𝑦(𝑦𝐴𝑥 = 𝑦)))
61, 3, 53bitr4i 303 . . 3 (∀𝑦((𝑥𝐴𝑦𝐴) → 𝑥 = 𝑦) ↔ (𝑥𝐴 → ∀𝑦𝐴 𝑥 = 𝑦))
76albii 1822 . 2 (∀𝑥𝑦((𝑥𝐴𝑦𝐴) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐴 𝑥 = 𝑦))
8 eleq1w 2821 . . 3 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
98mo4 2566 . 2 (∃*𝑥 𝑥𝐴 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → 𝑥 = 𝑦))
10 df-ral 3069 . 2 (∀𝑥𝐴𝑦𝐴 𝑥 = 𝑦 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐴 𝑥 = 𝑦))
117, 9, 103bitr4i 303 1 (∃*𝑥 𝑥𝐴 ↔ ∀𝑥𝐴𝑦𝐴 𝑥 = 𝑦)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wal 1537  wcel 2106  ∃*wmo 2538  wral 3064
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 1913  ax-6 1971  ax-7 2011  ax-8 2108
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-mo 2540  df-clel 2816  df-ral 3069
This theorem is referenced by:  disjnf  30906  isthinc3  46271  isthincd2lem1  46275  mndtcbas2  46337
  Copyright terms: Public domain W3C validator