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

Theorem isseti 2608
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 2606 . 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 1285   E.wex 1422    e. wcel 1434   _Vcvv 2602
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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-v 2604
This theorem is referenced by:  rexcom4b  2625  ceqsex  2638  vtoclf  2653  vtocl2  2655  vtocl3  2656  vtoclef  2672  eqvinc  2719  euind  2780  opabm  4043  eusv2nf  4214  dtruex  4310  limom  4362  isarep2  5017  dfoprab2  5583  rnoprab  5618  dmaddpq  6631  dmmulpq  6632  bj-inf2vnlem1  10950
  Copyright terms: Public domain W3C validator