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

Theorem moeq 3226
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 3061 . . . 4  |-  ( A  e.  _V  <->  E. x  x  =  A )
2 eueq 3222 . . . 4  |-  ( A  e.  _V  <->  E! x  x  =  A )
31, 2bitr3i 259 . . 3  |-  ( E. x  x  =  A  <-> 
E! x  x  =  A )
43biimpi 199 . 2  |-  ( E. x  x  =  A  ->  E! x  x  =  A )
5 df-mo 2315 . 2  |-  ( E* x  x  =  A  <-> 
( E. x  x  =  A  ->  E! x  x  =  A
) )
64, 5mpbir 214 1  |-  E* x  x  =  A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455   E.wex 1674    e. wcel 1898   E!weu 2310   E*wmo 2311   _Vcvv 3057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-v 3059
This theorem is referenced by:  mosub  3228  euxfr2  3235  reueq  3248  rmoeq  3249  sndisj  4410  disjxsn  4412  reusv1  4620  reusv2lem1  4621  reuxfr2d  4640  funopabeq  5639  funcnvsn  5650  fvmptg  5974  fvopab6  6003  ovmpt4g  6451  ov3  6465  ov6g  6466  oprabex3  6814  1stconst  6916  2ndconst  6917  iunmapdisj  8485  axaddf  9600  axmulf  9601  joinfval  16302  joinval  16306  meetfval  16316  meetval  16320  reuxfr3d  28181  abrexdom2jm  28198  abrexdom2  32104
  Copyright terms: Public domain W3C validator