ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  isseti Unicode version

Theorem isseti 2621
Description: A way to say " A is a set" (inference rule). (Contributed by NM, 5-Aug-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 2619 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
31, 2mpbi 143 1  |-  E. x  x  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1287   E.wex 1424    e. wcel 1436   _Vcvv 2615
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-v 2617
This theorem is referenced by:  rexcom4b  2638  ceqsex  2651  vtoclf  2666  vtocl2  2668  vtocl3  2669  vtoclef  2685  eqvinc  2731  euind  2793  opabm  4080  eusv2nf  4251  dtruex  4347  limom  4400  isarep2  5063  dfoprab2  5647  rnoprab  5682  dmaddpq  6875  dmmulpq  6876  bj-inf2vnlem1  11295
  Copyright terms: Public domain W3C validator