Theorem isset 3456

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

Syntax hints:   ↔ wb 205   = wceq 1541  ∃wex 1781   ∈ wcel 2106  Vcvv 3443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3445

This theorem is referenced by:  issetf  3457  issetri  3459  elex  3461  eueq  3664  ru  3736  sbc5ALT  3766  snprc  4676  snssb  4741  vprc  5270  eusvnfb  5346  reusv2lem3  5353  iotaexOLD  6473  funimaexgOLD  6585  fvmptd3f  6960  fvmptdv2  6963  ovmpodf  7507  rankf  9726  fnpr2ob  17432  isssc  17695  lrrecfr  27239  snelsingles  34474  bj-snglex  35411  bj-abex  35468  bj-clex  35469  bj-nul  35494  dissneqlem  35778  wl-issetft  36001  snen1g  41738  rr-spce  42419  iotaexeu  42640  elnev  42660  ax6e2nd  42782  ax6e2ndVD  43132  ax6e2ndALT  43154  upbdrech  43475  itgsubsticclem  44148