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

Theorem isset 2606
Description: Two ways to say " A is a set": A class  A is a member of the universal class  _V (see df-v 2604) if and only if the class  A exists (i.e. there exists some set  x equal to class 
A). Theorem 6.9 of [Quine] p. 43. Notational convention: We will use the notational device " A  e.  _V " to mean " A is a set" very frequently, for example in uniex 4194. Note the when  A is not a set, it is called a proper class. In some theorems, such as uniexg 4195, in order to shorten certain proofs we use the more general antecedent  A  e.  V instead of  A  e.  _V to mean " A is a set."

Note that a constant is implicitly considered distinct from all variables. This is why  _V is not included in the distinct variable list, even though df-clel 2078 requires that the expression substituted for  B not contain  x. (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 26-May-1993.)

Assertion
Ref Expression
isset  |-  ( A  e.  _V  <->  E. x  x  =  A )
Distinct variable group:    x, A

Proof of Theorem isset
StepHypRef Expression
1 df-clel 2078 . 2  |-  ( A  e.  _V  <->  E. x
( x  =  A  /\  x  e.  _V ) )
2 vex 2605 . . . 4  |-  x  e. 
_V
32biantru 296 . . 3  |-  ( x  =  A  <->  ( x  =  A  /\  x  e.  _V ) )
43exbii 1537 . 2  |-  ( E. x  x  =  A  <->  E. x ( x  =  A  /\  x  e. 
_V ) )
51, 4bitr4i 185 1  |-  ( A  e.  _V  <->  E. x  x  =  A )
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103    = 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:  issetf  2607  isseti  2608  issetri  2609  elex  2611  elisset  2614  ceqex  2723  eueq  2764  moeq  2768  mosubt  2770  ru  2815  sbc5  2839  snprc  3459  vprc  3911  vnex  3913  opelopabsb  4017  eusvnfb  4206  euiotaex  4907  fvmptdf  5284  fvmptdv2  5286  fmptco  5356  brabvv  5576  ovmpt2df  5657  ovi3  5662  tfrlemibxssdm  5970  tfr1onlembxssdm  5986  tfrcllembxssdm  5999  ecexr  6170  bj-vprc  10830  bj-vnex  10832  bj-2inf  10876
  Copyright terms: Public domain W3C validator