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

Theorem moeq 3247
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 3085 . . . 4  |-  ( A  e.  _V  <->  E. x  x  =  A )
2 eueq 3243 . . . 4  |-  ( A  e.  _V  <->  E! x  x  =  A )
31, 2bitr3i 254 . . 3  |-  ( E. x  x  =  A  <-> 
E! x  x  =  A )
43biimpi 197 . 2  |-  ( E. x  x  =  A  ->  E! x  x  =  A )
5 df-mo 2270 . 2  |-  ( E* x  x  =  A  <-> 
( E. x  x  =  A  ->  E! x  x  =  A
) )
64, 5mpbir 212 1  |-  E* x  x  =  A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   E.wex 1659    e. wcel 1868   E!weu 2265   E*wmo 2266   _Vcvv 3081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-v 3083
This theorem is referenced by:  mosub  3249  euxfr2  3256  reueq  3269  sndisj  4412  disjxsn  4414  reusv1  4620  reusv2lem1  4621  reuxfr2d  4640  funopabeq  5631  funcnvsn  5642  fvmptg  5958  fvopab6  5986  ovmpt4g  6429  ov3  6443  ov6g  6444  oprabex3  6792  1stconst  6891  2ndconst  6892  iunmapdisj  8454  axaddf  9569  axmulf  9570  joinfval  16232  joinval  16236  meetfval  16246  meetval  16250  reuxfr3d  28108  abrexdom2jm  28126  abrexdom2  31969
  Copyright terms: Public domain W3C validator