Theorem isset 3411

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

Step	Hyp	Ref	Expression
1		dfclel 2810	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
2		vex 3402	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantru 533	. . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V))
4	3	exbii 1855	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
5	1, 4	bitr4i 281	1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1543  ∃wex 1787   ∈ wcel 2112  Vcvv 3398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400

This theorem is referenced by:  issetf  3412  issetri  3414  elex  3416  eueq  3610  ru  3682  sbc5ALT  3712  snprc  4619  vprc  5193  eusvnfb  5271  reusv2lem3  5278  iotaex  6338  funimaexg  6444  fvmptd3f  6811  fvmptdv2  6814  ovmpodf  7343  rankf  9375  fnpr2ob  17017  isssc  17279  lrrecfr  33786  snelsingles  33910  bj-snglex  34849  bj-nul  34913  dissneqlem  35197  snen1g  40757  rr-spce  41434  iotaexeu  41650  elnev  41670  ax6e2nd  41792  ax6e2ndVD  42142  ax6e2ndALT  42164  upbdrech  42458  itgsubsticclem  43134