Theorem isset 2864

Description: Two ways to say "A is a set": A class A is a member of the universal class V (see df-v 2862) 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 ∈ V " to mean "A is a set" very frequently, for example in uniex 4318. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 4317, in order to shorten certain proofs we use the more general antecedent A ∈ V instead of A ∈ 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 2349 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 ∈ V ↔ ∃x x = A)

Distinct variable group:   x,A

Proof of Theorem isset

Step	Hyp	Ref	Expression
1		df-clel 2349	. 2 ⊢ (A ∈ V ↔ ∃x(x = A ∧ x ∈ V))
2		vex 2863	. . . 4 ⊢ x ∈ V
3	2	biantru 491	. . 3 ⊢ (x = A ↔ (x = A ∧ x ∈ V))
4	3	exbii 1582	. 2 ⊢ (∃x x = A ↔ ∃x(x = A ∧ x ∈ V))
5	1, 4	bitr4i 243	1 ⊢ (A ∈ V ↔ ∃x x = A)

Syntax hints:   ↔ wb 176   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2862

This theorem is referenced by:  issetf  2865  isseti  2866  issetri  2867  elex  2868  elisset  2870  ceqex  2970  eueq  3009  moeq  3013  ru  3046  sbc5  3071  snprc  3789  ninexg  4098  snex  4112  1cex  4143  xpkvexg  4286  iotaex  4357  opeqexb  4621  eloprabga  5579  dmmpt  5684  fnce  6177