Theorem isset 3464

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  issetft  3466  issetri  3469  elex  3471  eueq  3666  ru  3738  sbc5ALT  3768  sbccomlem  3817  snprc  4678  snssb  4743  vprcOLD  5278  eusvnfb  5358  reusv2lem3  5365  fvmptd3f  7002  fvmptdv2  7005  ovmpodf  7569  rankf  9776  fnpr2ob  17644  isssc  17909  lrrecfr  28208  snelsingles  36499  bj-sbcex  37381  bj-inex1gALT  37668  bj-snglex  37717  bj-abex  37774  bj-clex  37775  bj-nul  37800  dissneqlem  38094  wl-issetft  38345  snen1g  44364  rr-spce  45042  iotaexeu  45242  elnev  45261  ax6e2nd  45381  ax6e2ndVD  45730  ax6e2ndALT  45752  upbdrech  46138  itgsubsticclem  46803