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

Theorem isseti 3084
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 3082 . 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 1370   E.wex 1587    e. wcel 1758   _Vcvv 3078
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3080
This theorem is referenced by:  rexcom4b  3100  ceqsex  3114  vtoclf  3129  vtocl2  3131  vtocl3  3132  vtoclef  3151  eqvinc  3193  euind  3253  eusv2nf  4599  zfpair  4638  axpr  4639  opabn0  4728  isarep2  5607  dfoprab2  6243  rnoprab  6284  ov3  6338  omeu  7135  cflem  8527  genpass  9290  supmul1  10407  supmullem2  10409  supmul  10410  uzindOLD  10848  ruclem13  13643  joindm  15293  meetdm  15307  supaddc  28566  supadd  28567  ac6s6f  29134  funressnfv  30183  bnj986  32280  bj-snsetex  32789
  Copyright terms: Public domain W3C validator