Theorem isset 3488

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

Syntax hints:   ↔ wb 205   = wceq 1542  ∃wex 1782   ∈ wcel 2107  Vcvv 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477

This theorem is referenced by:  issetf  3489  issetri  3491  elex  3493  eueq  3703  ru  3775  sbc5ALT  3805  snprc  4720  snssb  4785  vprc  5314  eusvnfb  5390  reusv2lem3  5397  iotaexOLD  6520  funimaexgOLD  6632  fvmptd3f  7009  fvmptdv2  7012  ovmpodf  7559  rankf  9785  fnpr2ob  17500  isssc  17763  lrrecfr  27407  snelsingles  34832  bj-snglex  35792  bj-abex  35849  bj-clex  35850  bj-nul  35875  dissneqlem  36159  wl-issetft  36382  snen1g  42208  rr-spce  42889  iotaexeu  43110  elnev  43130  ax6e2nd  43252  ax6e2ndVD  43602  ax6e2ndALT  43624  upbdrech  43950  itgsubsticclem  44626