Theorem isset 3359

Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3353) 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 7098. Note that a class 𝐴 which is not a set is called a proper class. In some theorems, such as uniexg 7100, 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 2767 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 2767	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
2		vex 3354	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantru 519	. . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V))
4	3	exbii 1924	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
5	1, 4	bitr4i 267	1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Syntax hints:   ↔ wb 196   ∧ wa 382   = wceq 1631  ∃wex 1852   ∈ wcel 2145  Vcvv 3351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-tru 1634  df-ex 1853  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-v 3353

This theorem is referenced by:  issetf  3360  isseti  3361  issetri  3362  elex  3364  elisset  3367  vtoclg1f  3416  eueq  3530  moeq  3534  ru  3586  sbc5  3612  snprc  4389  vprc  4931  eusvnfb  4993  reusv2lem3  5000  iotaex  6009  funimaexg  6113  fvmptd3f  6435  fvmptdv2  6438  ovmpt2df  6937  rankf  8819  isssc  16680  dmscut  32248  snelsingles  32359  bj-snglex  33285  bj-nul  33342  dissneqlem  33517  iotaexeu  39138  elnev  39158  ax6e2nd  39292  ax6e2ndVD  39659  ax6e2ndALT  39681  upbdrech  40029  itgsubsticclem  40701