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

Theorem moeq 3272
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 3110 . . . 4  |-  ( A  e.  _V  <->  E. x  x  =  A )
2 eueq 3268 . . . 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 2289 . 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 1398   E.wex 1617    e. wcel 1823   E!weu 2284   E*wmo 2285   _Vcvv 3106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3108
This theorem is referenced by:  mosub  3274  euxfr2  3281  reueq  3294  sndisj  4431  disjxsn  4433  reusv1  4637  reusv2lem1  4638  reuxfr2d  4660  funopabeq  5604  funcnvsn  5615  fvmptg  5929  fvopab6  5956  ovmpt4g  6398  ov3  6412  ov6g  6413  oprabex3  6762  1stconst  6861  2ndconst  6862  iunmapdisj  8395  axaddf  9511  axmulf  9512  joinfval  15830  joinval  15834  meetfval  15844  meetval  15848  reuxfr3d  27586  abrexdom2jm  27605  abrexdom2  30462
  Copyright terms: Public domain W3C validator