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

Theorem isset 2961
Description: Two ways to say " A is a set": A class  A is a member of the universal class  _V (see df-v 2959) 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 4706. Note the when  A is not a set, it is called a proper class. In some theorems, such as uniexg 4707, 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 2433 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, 5-Aug-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 2433 . 2  |-  ( A  e.  _V  <->  E. x
( x  =  A  /\  x  e.  _V ) )
2 vex 2960 . . . 4  |-  x  e. 
_V
32biantru 493 . . 3  |-  ( x  =  A  <->  ( x  =  A  /\  x  e.  _V ) )
43exbii 1593 . 2  |-  ( E. x  x  =  A  <->  E. x ( x  =  A  /\  x  e. 
_V ) )
51, 4bitr4i 245 1  |-  ( A  e.  _V  <->  E. x  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1551    = wceq 1653    e. wcel 1726   _Vcvv 2957
This theorem is referenced by:  issetf  2962  isseti  2963  issetri  2964  elex  2965  elisset  2967  ceqex  3067  eueq  3107  moeq  3111  ru  3161  sbc5  3186  snprc  3872  vprc  4342  vnex  4344  eusvnfb  4720  reusv2lem3  4727  iotaex  5436  funimaexg  5531  fvmptdf  5817  fvmptdv2  5819  ovmpt2df  6206  rankf  7721  isssc  14021  snelsingles  25768  ceqsex3OLD  26710  iotaexeu  27596  elnev  27616  a9e2nd  28646  a9e2ndVD  29021  a9e2ndALT  29043
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-v 2959
  Copyright terms: Public domain W3C validator