Theorem isset 3113

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

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

Assertion

Ref	Expression
isset

Distinct variable group:   ,

Proof of Theorem isset

Step	Hyp	Ref	Expression
1		df-clel 2452	. 2
2		vex 3112	. . . 4
3	2	biantru 505	. . 3
4	3	exbii 1667	. 2
5	1, 4	bitr4i 252	1

Syntax hints:  <->wb 184  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818  cvv 3109

This theorem is referenced by:  issetf  3114  isseti  3115  issetri  3116  elex  3118  elisset  3120  vtoclg1f  3166  eueq  3271  moeq  3275  ru  3326  sbc5  3352  snprc  4093  vprc  4590  vnex  4592  eusvnfb  4648  reusv2lem3  4655  iotaex  5573  funimaexg  5670  fvmptdf  5967  fvmptdv2  5969  ovmpt2df  6434  rankf  8233  isssc  15189  snelsingles  29572  ceqsex3OLD  30601  iotaexeu  31325  elnev  31345  upbdrech  31505  itgsubsticclem  31774  ax6e2nd  33331  ax6e2ndVD  33708  ax6e2ndALT  33730  bj-snglex  34531  bj-nul  34585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111