ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  moeq Unicode version

Theorem moeq 2788
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 2625 . . . 4  |-  ( A  e.  _V  <->  E. x  x  =  A )
2 eueq 2784 . . . 4  |-  ( A  e.  _V  <->  E! x  x  =  A )
31, 2bitr3i 184 . . 3  |-  ( E. x  x  =  A  <-> 
E! x  x  =  A )
43biimpi 118 . 2  |-  ( E. x  x  =  A  ->  E! x  x  =  A )
5 df-mo 1952 . 2  |-  ( E* x  x  =  A  <-> 
( E. x  x  =  A  ->  E! x  x  =  A
) )
64, 5mpbir 144 1  |-  E* x  x  =  A
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1289   E.wex 1426    e. wcel 1438   E!weu 1948   E*wmo 1949   _Vcvv 2619
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-v 2621
This theorem is referenced by:  euxfr2dc  2798  reueq  2812  mosn  3474  sndisj  3833  disjxsn  3835  reusv1  4271  funopabeq  5036  funcnvsn  5045  fvmptg  5364  fvopab6  5380  ovmpt4g  5749  ovi3  5763  ov6g  5764  oprabex3  5882  1stconst  5968  2ndconst  5969
  Copyright terms: Public domain W3C validator