Theorem isset 3502

Description: Two ways to express that "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3490) 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 7776. 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 7775 compared with uniex 7776). That this is more general is seen either by substitution (when the variable 𝑉 has no other occurrences), or by elex 3509. (Contributed by NM, 26-May-1993.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

Syntax hints:   ↔ wb 206   = wceq 1537  ∃wex 1777   ∈ wcel 2108  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490

This theorem is referenced by:  issetft  3504  issetri  3507  elex  3509  elexOLD  3510  eueq  3730  ru  3802  ruOLD  3803  sbc5ALT  3833  sbccomlem  3891  snprc  4742  snssb  4807  vprc  5333  eusvnfb  5411  reusv2lem3  5418  iotaexOLD  6553  funimaexgOLD  6665  fvmptd3f  7044  fvmptdv2  7047  ovmpodf  7606  rankf  9863  fnpr2ob  17618  isssc  17881  lrrecfr  27994  snelsingles  35886  bj-snglex  36939  bj-abex  36996  bj-clex  36997  bj-nul  37022  dissneqlem  37306  wl-issetft  37536  snen1g  43486  rr-spce  44166  iotaexeu  44387  elnev  44407  ax6e2nd  44529  ax6e2ndVD  44879  ax6e2ndALT  44901  upbdrech  45220  itgsubsticclem  45896