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

Theorem isseti 2898
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 2896 . 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 1547    = wceq 1649    e. wcel 1717   _Vcvv 2892
This theorem is referenced by:  rexcom4b  2913  ceqsex  2926  vtoclf  2941  vtocl2  2943  vtocl3  2944  vtoclef  2960  eqvinc  2999  euind  3057  zfpair  4335  axpr  4336  opabn0  4419  eusv2nf  4654  isarep2  5466  dfoprab2  6053  rnoprab  6088  ov3  6142  omeu  6757  cflem  8052  genpass  8812  supmul1  9898  supmullem2  9900  supmul  9901  uzindOLD  10289  ruclem13  12761  supaddc  25940  supadd  25941  funressnfv  27654  bnj986  28656
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-v 2894
  Copyright terms: Public domain W3C validator