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

Theorem isseti 3028
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 3026 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
31, 2mpbi 211 1  |-  E. x  x  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   E.wex 1657    e. wcel 1872   _Vcvv 3022
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-12 1909  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-v 3024
This theorem is referenced by:  rexcom4b  3045  ceqsex  3059  vtoclf  3074  vtocl  3075  vtocl2  3077  vtocl3  3078  vtoclef  3097  eqvinc  3141  euind  3200  eusv2nf  4565  zfpair  4601  axpr  4602  opabn0  4694  isarep2  5624  dfoprab2  6295  rnoprab  6337  ov3  6391  omeu  7241  cflem  8627  genpass  9385  supaddc  10525  supadd  10526  supmul1  10527  supmullem2  10529  supmul  10530  ruclem13  14237  joindm  16192  meetdm  16206  bnj986  29717  bj-snsetex  31468  ac6s6f  32323  elintima  36158  funressnfv  38443
  Copyright terms: Public domain W3C validator