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

Theorem isset 2920
Description: Two ways to say " A is a set": A class  A is a member of the universal class  _V (see df-v 2918) 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 4664. Note the when  A is not a set, it is called a proper class. In some theorems, such as uniexg 4665, 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 2400 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 2400 . 2  |-  ( A  e.  _V  <->  E. x
( x  =  A  /\  x  e.  _V ) )
2 vex 2919 . . . 4  |-  x  e. 
_V
32biantru 492 . . 3  |-  ( x  =  A  <->  ( x  =  A  /\  x  e.  _V ) )
43exbii 1589 . 2  |-  ( E. x  x  =  A  <->  E. x ( x  =  A  /\  x  e. 
_V ) )
51, 4bitr4i 244 1  |-  ( A  e.  _V  <->  E. x  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1547    = wceq 1649    e. wcel 1721   _Vcvv 2916
This theorem is referenced by:  issetf  2921  isseti  2922  issetri  2923  elex  2924  elisset  2926  ceqex  3026  eueq  3066  moeq  3070  ru  3120  sbc5  3145  snprc  3831  vprc  4301  vnex  4303  eusvnfb  4678  reusv2lem3  4685  iotaex  5394  funimaexg  5489  fvmptdf  5775  fvmptdv2  5777  ovmpt2df  6164  rankf  7676  isssc  13975  snelsingles  25675  ceqsex3OLD  26599  iotaexeu  27486  elnev  27506  a9e2nd  28356  a9e2ndVD  28729  a9e2ndALT  28752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-v 2918
  Copyright terms: Public domain W3C validator