Theorem isset 3193

Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3188) 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 6906. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 6908, 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 2617 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 2617	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
2		vex 3189	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantru 526	. . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V))
4	3	exbii 1771	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
5	1, 4	bitr4i 267	1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1480  ∃wex 1701   ∈ wcel 1987  Vcvv 3186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-12 2044  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1483  df-ex 1702  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3188

This theorem is referenced by:  issetf  3194  isseti  3195  issetri  3196  elex  3198  elisset  3201  vtoclg1f  3251  eueq  3360  moeq  3364  ru  3416  sbc5  3442  snprc  4223  vprc  4756  vnex  4758  eusvnfb  4822  reusv2lem3  4831  iotaex  5827  funimaexg  5933  fvmptdf  6252  fvmptdv2  6254  ovmpt2df  6745  rankf  8601  isssc  16401  snelsingles  31668  bj-snglex  32605  bj-nul  32662  dissneqlem  32816  iotaexeu  38098  elnev  38118  ax6e2nd  38253  ax6e2ndVD  38624  ax6e2ndALT  38646  upbdrech  38980  itgsubsticclem  39495