Theorem isseti 3181

Description: A way to say "𝐴 is a set" (inference rule). (Contributed by NM, 24-Jun-1993.)

Hypothesis

Ref	Expression
isseti.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
isseti	⊢ ∃𝑥 𝑥 = 𝐴

Distinct variable group:   𝑥,𝐴

Proof of Theorem isseti

Step	Hyp	Ref	Expression
1		isseti.1	. 2 ⊢ 𝐴 ∈ V
2		isset 3179	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
3	1, 2	mpbi 218	1 ⊢ ∃𝑥 𝑥 = 𝐴

Syntax hints:   = wceq 1474  ∃wex 1694   ∈ wcel 1976  Vcvv 3172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-v 3174

This theorem is referenced by:  rexcom4b  3199  ceqsex  3213  vtoclf  3230  vtocl  3231  vtocl2  3233  vtocl3  3234  vtoclef  3253  eqvinc  3299  euind  3359  eusv2nf  4785  zfpair  4826  axpr  4827  opabn0  4921  isarep2  5878  dfoprab2  6577  rnoprab  6619  ov3  6673  omeu  7530  cflem  8929  genpass  9688  supaddc  10840  supadd  10841  supmul1  10842  supmullem2  10844  supmul  10845  ruclem13  14759  joindm  16775  meetdm  16789  bnj986  30112  bj-snsetex  31968  bj-restn0  32048  bj-restuni  32055  ac6s6f  32975  elintima  36788  funressnfv  39681