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

Theorem moeq 3229
Description: There is at most one set equal to a class. (Contributed by NM, 8-Mar-1995.)
Assertion
Ref Expression
moeq  |-  E* x  x  =  A
Distinct variable group:    x, A

Proof of Theorem moeq
StepHypRef Expression
1 isset 3069 . . . 4  |-  ( A  e.  _V  <->  E. x  x  =  A )
2 eueq 3225 . . . 4  |-  ( A  e.  _V  <->  E! x  x  =  A )
31, 2bitr3i 251 . . 3  |-  ( E. x  x  =  A  <-> 
E! x  x  =  A )
43biimpi 194 . 2  |-  ( E. x  x  =  A  ->  E! x  x  =  A )
5 df-mo 2265 . 2  |-  ( E* x  x  =  A  <-> 
( E. x  x  =  A  ->  E! x  x  =  A
) )
64, 5mpbir 209 1  |-  E* x  x  =  A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370   E.wex 1587    e. wcel 1758   E!weu 2260   E*wmo 2261   _Vcvv 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-v 3067
This theorem is referenced by:  mosub  3231  euxfr2  3238  reueq  3251  sndisj  4379  disjxsn  4381  reusv1  4587  reusv2lem1  4588  reuxfr2d  4610  funopabeq  5547  funcnvsn  5558  fvmptg  5868  fvopab6  5892  ovmpt4g  6310  ov3  6324  ov6g  6325  oprabex3  6663  1stconst  6758  2ndconst  6759  iunmapdisj  8291  axaddf  9410  axmulf  9411  joinfval  15270  joinval  15274  meetfval  15284  meetval  15288  reuxfr3d  26005  abrexdom2jm  26021  abrexdom2  28760
  Copyright terms: Public domain W3C validator