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

Theorem moeq 3368
 Description: There is at most one set equal to a class. (Contributed by NM, 8-Mar-1995.)
Assertion
Ref Expression
moeq ∃*𝑥 𝑥 = 𝐴
Distinct variable group:   𝑥,𝐴

Proof of Theorem moeq
StepHypRef Expression
1 isset 3196 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
2 eueq 3364 . . 3 (𝐴 ∈ V ↔ ∃!𝑥 𝑥 = 𝐴)
31, 2sylbb1 227 . 2 (∃𝑥 𝑥 = 𝐴 → ∃!𝑥 𝑥 = 𝐴)
4 df-mo 2474 . 2 (∃*𝑥 𝑥 = 𝐴 ↔ (∃𝑥 𝑥 = 𝐴 → ∃!𝑥 𝑥 = 𝐴))
53, 4mpbir 221 1 ∃*𝑥 𝑥 = 𝐴
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1480  ∃wex 1701   ∈ wcel 1987  ∃!weu 2469  ∃*wmo 2470  Vcvv 3189 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-clab 2608  df-cleq 2614  df-clel 2617  df-v 3191 This theorem is referenced by:  mosub  3370  euxfr2  3377  reueq  3390  rmoeq  3391  sndisj  4609  disjxsn  4611  reusv1OLD  4832  reuxfr2d  4856  funopabeq  5887  funcnvsn  5899  fvmptg  6242  fvopab6  6271  ovmpt4g  6743  ov3  6757  ov6g  6758  oprabex3  7109  1stconst  7217  2ndconst  7218  iunmapdisj  8798  axaddf  9918  axmulf  9919  joinfval  16933  joinval  16937  meetfval  16947  meetval  16951  reuxfr3d  29200  abrexdom2jm  29216  abrexdom2  33193
 Copyright terms: Public domain W3C validator