Theorem isset 3207

Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3202) if and only if the class 𝐴 exists (i.e. there exists some set 𝑥 equal to class 𝐴). Theorem 6.9 of [Quine] p. 43. Notational convention: We will use the notational device "𝐴 ∈ V " to mean "𝐴 is a set" very frequently, for example in uniex 6953. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 6955, in order to shorten certain proofs we use the more general antecedent 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to mean "𝐴 is a set."

Note that a constant is implicitly considered distinct from all variables. This is why V is not included in the distinct variable list, even though df-clel 2618 requires that the expression substituted for 𝐵 not contain 𝑥. (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 26-May-1993.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

Step	Hyp	Ref	Expression
1		df-clel 2618	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
2		vex 3203	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantru 526	. . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V))
4	3	exbii 1774	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
5	1, 4	bitr4i 267	1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990  Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  issetf  3208  isseti  3209  issetri  3210  elex  3212  elisset  3215  vtoclg1f  3265  eueq  3378  moeq  3382  ru  3434  sbc5  3460  snprc  4253  vprc  4796  vnex  4798  eusvnfb  4862  reusv2lem3  4871  iotaex  5868  funimaexg  5975  fvmptd3f  6295  fvmptdv2  6298  ovmpt2df  6792  rankf  8657  isssc  16480  dmscut  31918  snelsingles  32029  bj-snglex  32961  bj-nul  33018  dissneqlem  33187  iotaexeu  38619  elnev  38639  ax6e2nd  38774  ax6e2ndVD  39144  ax6e2ndALT  39166  upbdrech  39519  itgsubsticclem  40191