Theorem isset 3451

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

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

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

Syntax hints:   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2113  Vcvv 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439

This theorem is referenced by:  issetft  3453  issetri  3456  elex  3458  elexOLD  3459  eueq  3663  ru  3735  ruOLD  3736  sbc5ALT  3766  sbccomlem  3816  snprc  4671  snssb  4736  vprc  5257  eusvnfb  5335  reusv2lem3  5342  fvmptd3f  6953  fvmptdv2  6956  ovmpodf  7511  rankf  9698  fnpr2ob  17470  isssc  17735  lrrecfr  27906  snelsingles  36036  bj-snglex  37090  bj-abex  37147  bj-clex  37148  bj-nul  37173  dissneqlem  37457  wl-issetft  37699  snen1g  43681  rr-spce  44361  iotaexeu  44575  elnev  44594  ax6e2nd  44715  ax6e2ndVD  45064  ax6e2ndALT  45086  upbdrech  45469  itgsubsticclem  46135