Theorem isset 3468

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456

This theorem is used by:  issetft  3470  issetri  3473  elex  3475  eueq  3669  ru  3741  sbc5ALT  3771  sbccomlem  3821  snprc  4680  snssb  4745  vprcOLD  5282  eusvnfb  5362  reusv2lem3  5369  fvmptd3f  7040  fvmptdv2  7043  ovmpodf  7608  rankf  9839  fnpr2ob  17780  isssc  18045  lrrecfr  28386  snelsingles  36899  bj-sbcex  37765  bj-inex1gALT  38052  bj-snglex  38101  bj-abex  38158  bj-clex  38159  bj-nul  38241  dissneqlem  38531  wl-issetft  38782  snen1g  44786  rr-spce  45463  iotaexeu  45662  elnev  45681  ax6e2nd  45801  ax6e2ndVD  46150  ax6e2ndALT  46172  upbdrech  46594  itgsubsticclem  47258