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

Theorem isseti 2768
Description: A way to say " A is a set" (inference form). (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 2766 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
31, 2mpbi 145 1  |-  E. x  x  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1364   E.wex 1503    e. wcel 2164   _Vcvv 2760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2175
This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762
This theorem is referenced by:  rexcom4b  2785  ceqsex  2798  ceqsexv2d  2800  vtoclf  2814  vtocl2  2816  vtocl3  2817  vtoclef  2834  eqvinc  2884  euind  2948  opabm  4312  eusv2nf  4488  dtruex  4592  limom  4647  isarep2  5342  dfoprab2  5966  rnoprab  6002  dmaddpq  7441  dmmulpq  7442  bj-inf2vnlem1  15532
  Copyright terms: Public domain W3C validator