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 7760. 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 7759 compared with uniex 7760). 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 1569  ∃wex 1811   ∈ wcel 2144  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  issetft  3466  issetri  3469  elex  3471  eueq  3665  ru  3737  sbc5ALT  3767  sbccomlem  3817  snprc  4674  snssb  4739  vprcOLD  5274  eusvnfb  5354  reusv2lem3  5361  fvmptd3f  7012  fvmptdv2  7015  ovmpodf  7578  rankf  9807  fnpr2ob  17737  isssc  18002  lrrecfr  28336  snelsingles  36778  bj-sbcex  37644  bj-inex1gALT  37931  bj-snglex  37980  bj-abex  38037  bj-clex  38038  bj-nul  38077  dissneqlem  38370  wl-issetft  38621  snen1g  44632  rr-spce  45309  iotaexeu  45509  elnev  45528  ax6e2nd  45648  ax6e2ndVD  45997  ax6e2ndALT  46019  upbdrech  46428  itgsubsticclem  47092