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

Theorem isseti 3099
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 3097 . 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 1381   E.wex 1597    e. wcel 1802   _Vcvv 3093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-12 1838  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-v 3095
This theorem is referenced by:  rexcom4b  3115  ceqsex  3129  vtoclf  3144  vtocl2  3146  vtocl3  3147  vtoclef  3166  eqvinc  3210  euind  3270  eusv2nf  4631  zfpair  4670  axpr  4671  opabn0  4764  isarep2  5654  dfoprab2  6324  rnoprab  6366  ov3  6420  omeu  7232  cflem  8624  genpass  9385  supmul1  10509  supmullem2  10511  supmul  10512  uzindOLD  10958  ruclem13  13847  joindm  15502  meetdm  15516  supaddc  30009  supadd  30010  ac6s6f  30549  funressnfv  32047  bnj986  33719  bj-snsetex  34233
  Copyright terms: Public domain W3C validator