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

Theorem isset 2792
Description: Two ways to say " A is a set": A class  A is a member of the universal class  _V (see df-v 2790) 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 4516. Note the when  A is not a set, it is called a proper class. In some theorems, such as uniexg 4517, 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 2279 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 2279 . 2  |-  ( A  e.  _V  <->  E. x
( x  =  A  /\  x  e.  _V ) )
2 vex 2791 . . . 4  |-  x  e. 
_V
32biantru 491 . . 3  |-  ( x  =  A  <->  ( x  =  A  /\  x  e.  _V ) )
43exbii 1569 . 2  |-  ( E. x  x  =  A  <->  E. x ( x  =  A  /\  x  e. 
_V ) )
51, 4bitr4i 243 1  |-  ( A  e.  _V  <->  E. x  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1528    = wceq 1623    e. wcel 1684   _Vcvv 2788
This theorem is referenced by:  issetf  2793  isseti  2794  issetri  2795  elex  2796  elisset  2798  ceqex  2898  eueq  2937  moeq  2941  ru  2990  sbc5  3015  snprc  3695  vprc  4152  vnex  4154  eusvnfb  4530  reusv2lem3  4537  iotaex  5236  funimaexg  5329  fvmptdf  5611  fvmptdv2  5613  ovmpt2df  5979  rankf  7466  isssc  13697  snelsingles  24461  ceqsex3OLD  26726  iotaexeu  27618  elnev  27638  a9e2nd  28324  a9e2ndVD  28684  a9e2ndALT  28707
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790
  Copyright terms: Public domain W3C validator