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

Theorem isseti 3112
Description: A way to say " A is a set" (inference rule). (Contributed by NM, 24-Jun-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 3110 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
31, 2mpbi 208 1  |-  E. x  x  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398   E.wex 1617    e. wcel 1823   _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-12 1859  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3108
This theorem is referenced by:  rexcom4b  3128  ceqsex  3142  vtoclf  3157  vtocl2  3159  vtocl3  3160  vtoclef  3179  eqvinc  3223  euind  3283  eusv2nf  4635  zfpair  4674  axpr  4675  opabn0  4767  isarep2  5650  dfoprab2  6316  rnoprab  6358  ov3  6412  omeu  7226  cflem  8617  genpass  9376  supmul1  10503  supmullem2  10505  supmul  10506  uzindOLD  10953  ruclem13  14062  joindm  15835  meetdm  15849  supaddc  30284  supadd  30285  ac6s6f  30824  funressnfv  32455  bnj986  34432  bj-snsetex  34941  elintima  38198
  Copyright terms: Public domain W3C validator