Theorem isset 3508

Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3498) 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 7469. Note that a class 𝐴 which is not a set is called a proper class. In some theorems, such as uniexg 7468, 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 2895 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		dfclel 2896	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
2		vex 3499	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantru 532	. . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V))
4	3	exbii 1848	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
5	1, 4	bitr4i 280	1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114  Vcvv 3496

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-v 3498

This theorem is referenced by:  issetf  3509  issetiOLD  3511  issetri  3512  elex  3514  elissetOLD  3517  eueq  3701  ru  3773  sbc5  3802  snprc  4655  vprc  5221  eusvnfb  5296  reusv2lem3  5303  iotaex  6337  funimaexg  6442  fvmptd3f  6785  fvmptdv2  6788  ovmpodf  7308  rankf  9225  fnpr2ob  16833  isssc  17092  snelsingles  33385  bj-snglex  34287  bj-nul  34351  dissneqlem  34623  snen1g  39897  rr-spce  40564  iotaexeu  40757  elnev  40777  ax6e2nd  40899  ax6e2ndVD  41249  ax6e2ndALT  41271  upbdrech  41579  itgsubsticclem  42267