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

Theorem isseti 2954
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 2952 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
31, 2mpbi 200 1  |-  E. x  x  =  A
Colors of variables: wff set class
Syntax hints:   E.wex 1550    = wceq 1652    e. wcel 1725   _Vcvv 2948
This theorem is referenced by:  rexcom4b  2969  ceqsex  2982  vtoclf  2997  vtocl2  2999  vtocl3  3000  vtoclef  3016  eqvinc  3055  euind  3113  zfpair  4393  axpr  4394  opabn0  4477  eusv2nf  4713  isarep2  5525  dfoprab2  6113  rnoprab  6148  ov3  6202  omeu  6820  cflem  8118  genpass  8878  supmul1  9965  supmullem2  9967  supmul  9968  uzindOLD  10356  ruclem13  12833  supaddc  26228  supadd  26229  funressnfv  27959  bnj986  29262
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-v 2950
  Copyright terms: Public domain W3C validator