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

Theorem moeq 3540
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 3364 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
2 eueq 3536 . . 3 (𝐴 ∈ V ↔ ∃!𝑥 𝑥 = 𝐴)
31, 2sylbb1 228 . 2 (∃𝑥 𝑥 = 𝐴 → ∃!𝑥 𝑥 = 𝐴)
4 df-mo 2626 . 2 (∃*𝑥 𝑥 = 𝐴 ↔ (∃𝑥 𝑥 = 𝐴 → ∃!𝑥 𝑥 = 𝐴))
53, 4mpbir 222 1 ∃*𝑥 𝑥 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1634  wex 1855  wcel 2148  ∃!weu 2621  ∃*wmo 2622  Vcvv 3355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-v 3357
This theorem is referenced by:  mosub  3542  euxfr2  3549  reueq  3562  rmoeq  3563  sndisj  4789  disjxsn  4791  reuxfr2d  5033  funopabeq  6078  funcnvsn  6090  fvmptg  6439  fvopab6  6470  ovmpt4g  6951  ov3  6965  ov6g  6966  oprabex3  7325  1stconst  7437  2ndconst  7438  iunmapdisj  9067  axaddf  10189  axmulf  10190  joinfval  17229  joinval  17233  meetfval  17243  meetval  17247  reuxfr3d  29685  abrexdom2jm  29701  abrexdom2  33875
  Copyright terms: Public domain W3C validator