Theorem isset 3465

Description: Two ways to express that "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3453) if and only if the class 𝐴 exists (i.e., there exists some set 𝑥 equal to class 𝐴). Theorem 6.9 of [Quine] p. 43.

A class 𝐴 which is not a set is called a proper class.

Conventions: We will often use the expression "𝐴 ∈ V " to mean "𝐴 is a set", for example in uniex 7756. To make some theorems more readily applicable, we will also use the more general expression 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to mean "𝐴 is a set", typically in an antecedent, or in a hypothesis for theorems in deduction form (see for instance uniexg 7755 compared with uniex 7756). That this is more general is seen either by substitution (when the variable 𝑉 has no other occurrences), or by elex 3472. (Contributed by NM, 26-May-1993.)

Assertion

Ref	Expression
isset	⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

Step	Hyp	Ref	Expression
1		vex 3455	. 2 ⊢ 𝑥 ∈ V
2	1	issetlem 2841	1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453

This theorem is used by:  issetft  3467  issetri  3470  elex  3472  eueq  3666  ru  3738  sbc5ALT  3768  sbccomlem  3817  snprc  4678  snssb  4743  vprcOLD  5275  eusvnfb  5355  reusv2lem3  5362  fvmptd3f  7007  fvmptdv2  7010  ovmpodf  7574  rankf  9795  fnpr2ob  17723  isssc  17988  lrrecfr  28322  snelsingles  36664  bj-sbcex  37530  bj-inex1gALT  37817  bj-snglex  37866  bj-abex  37923  bj-clex  37924  bj-nul  37951  dissneqlem  38243  wl-issetft  38494  snen1g  44509  rr-spce  45187  iotaexeu  45387  elnev  45406  ax6e2nd  45526  ax6e2ndVD  45875  ax6e2ndALT  45897  upbdrech  46290  itgsubsticclem  46954