Theorem isset 3471

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459

This theorem is used by:  issetft  3473  issetri  3476  elex  3478  eueq  3673  ru  3745  sbc5ALT  3775  sbccomlem  3824  snprc  4685  snssb  4750  vprcOLD  5286  eusvnfb  5366  reusv2lem3  5373  fvmptd3f  7009  fvmptdv2  7012  ovmpodf  7572  rankf  9769  fnpr2ob  17630  isssc  17895  lrrecfr  28167  snelsingles  36425  bj-sbcex  37306  bj-inex1gALT  37593  bj-snglex  37642  bj-abex  37699  bj-clex  37700  bj-nul  37725  dissneqlem  38019  wl-issetft  38270  snen1g  44283  rr-spce  44961  iotaexeu  45161  elnev  45180  ax6e2nd  45300  ax6e2ndVD  45649  ax6e2ndALT  45671  upbdrech  46057  itgsubsticclem  46722