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

Theorem moeq 3415
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 3238 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
2 eueq 3411 . . 3 (𝐴 ∈ V ↔ ∃!𝑥 𝑥 = 𝐴)
31, 2sylbb1 227 . 2 (∃𝑥 𝑥 = 𝐴 → ∃!𝑥 𝑥 = 𝐴)
4 df-mo 2503 . 2 (∃*𝑥 𝑥 = 𝐴 ↔ (∃𝑥 𝑥 = 𝐴 → ∃!𝑥 𝑥 = 𝐴))
53, 4mpbir 221 1 ∃*𝑥 𝑥 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wex 1744  wcel 2030  ∃!weu 2498  ∃*wmo 2499  Vcvv 3231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233
This theorem is referenced by:  mosub  3417  euxfr2  3424  reueq  3437  rmoeq  3438  sndisj  4676  disjxsn  4678  reusv1OLD  4897  reuxfr2d  4921  funopabeq  5962  funcnvsn  5974  fvmptg  6319  fvopab6  6350  ovmpt4g  6825  ov3  6839  ov6g  6840  oprabex3  7199  1stconst  7310  2ndconst  7311  iunmapdisj  8884  axaddf  10004  axmulf  10005  joinfval  17048  joinval  17052  meetfval  17062  meetval  17066  reuxfr3d  29456  abrexdom2jm  29472  abrexdom2  33656
  Copyright terms: Public domain W3C validator