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

Theorem moeq 2941
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 2792 . . . 4  |-  ( A  e.  _V  <->  E. x  x  =  A )
2 eueq 2937 . . . 4  |-  ( A  e.  _V  <->  E! x  x  =  A )
31, 2bitr3i 242 . . 3  |-  ( E. x  x  =  A  <-> 
E! x  x  =  A )
43biimpi 186 . 2  |-  ( E. x  x  =  A  ->  E! x  x  =  A )
5 df-mo 2148 . 2  |-  ( E* x  x  =  A  <-> 
( E. x  x  =  A  ->  E! x  x  =  A
) )
64, 5mpbir 200 1  |-  E* x  x  =  A
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528    = wceq 1623    e. wcel 1684   E!weu 2143   E*wmo 2144   _Vcvv 2788
This theorem is referenced by:  mosub  2943  euxfr2  2950  reueq  2962  sndisj  4015  disjxsn  4017  reusv1  4534  reusv2lem1  4535  reuxfr2d  4557  funopabeq  5288  funcnvsn  5297  fvmptg  5600  fvopab6  5621  oprabex3  5962  ovmpt4g  5970  ov3  5984  ov6g  5985  1stconst  6207  2ndconst  6208  iunmapdisj  7650  axaddf  8767  axmulf  8768  reuxfr3d  23138  abrexdom2jm  23166  cmp2morp  25958  cmpmorfun  25971  abrexdom2  26406
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790
  Copyright terms: Public domain W3C validator