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

Theorem isseti 3062
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 3060 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
31, 2mpbi 213 1  |-  E. x  x  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1454   E.wex 1673    e. wcel 1897   _Vcvv 3056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-12 1943  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-v 3058
This theorem is referenced by:  rexcom4b  3080  ceqsex  3094  vtoclf  3110  vtocl  3111  vtocl2  3113  vtocl3  3114  vtoclef  3133  eqvinc  3177  euind  3236  eusv2nf  4614  zfpair  4650  axpr  4651  opabn0  4745  isarep2  5684  dfoprab2  6363  rnoprab  6405  ov3  6459  omeu  7311  cflem  8701  genpass  9459  supaddc  10601  supadd  10602  supmul1  10603  supmullem2  10605  supmul  10606  ruclem13  14342  joindm  16297  meetdm  16311  bnj986  29813  bj-snsetex  31601  ac6s6f  32460  elintima  36289  funressnfv  38666
  Copyright terms: Public domain W3C validator