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

Theorem isseti 2794
Description: A way to say " A is a set" (inference rule). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
isseti.1  |-  A  e. 
_V
Assertion
Ref Expression
isseti  |-  E. x  x  =  A
Distinct variable group:    x, A

Proof of Theorem isseti
StepHypRef Expression
1 isseti.1 . 2  |-  A  e. 
_V
2 isset 2792 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
31, 2mpbi 199 1  |-  E. x  x  =  A
Colors of variables: wff set class
Syntax hints:   E.wex 1528    = wceq 1623    e. wcel 1684   _Vcvv 2788
This theorem is referenced by:  rexcom4b  2809  ceqsex  2822  vtoclf  2837  vtocl2  2839  vtocl3  2840  vtoclef  2856  eqvinc  2895  euind  2952  zfpair  4212  axpr  4213  opabn0  4295  eusv2nf  4532  isarep2  5332  dfoprab2  5895  rnoprab  5930  ov3  5984  omeu  6583  cflem  7872  genpass  8633  supmul1  9719  supmullem2  9721  supmul  9722  uzindOLD  10106  ruclem13  12520  dmoprabss6  25035  cmppar2  25972  bnj986  28986
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-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790
  Copyright terms: Public domain W3C validator