Theorem isseti 3437

Description: A way to say "𝐴 is a set" (inference form). (Contributed by NM, 24-Jun-1993.) Remove dependencies on axioms. (Revised by BJ, 13-Jul-2019.)

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		elissetv 2819	. 2 ⊢ (𝐴 ∈ V → ∃𝑥 𝑥 = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ ∃𝑥 𝑥 = 𝐴

Syntax hints:   = wceq 1539  ∃wex 1783   ∈ wcel 2108  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-clel 2817

This theorem is referenced by:  rexcom4b  3451  ceqsalv  3457  ceqsex  3468  ceqsexv  3469  vtoclf  3487  vtocl  3488  vtoclef  3513  euind  3654  eusv2nf  5313  zfpair  5339  axprALT  5340  opabn0  5459  isarep2  6507  dfoprab2  7311  rnoprab  7356  ov3  7413  omeu  8378  cflem  9933  genpass  10696  supaddc  11872  supadd  11873  supmul1  11874  supmullem2  11876  supmul  11877  ruclem13  15879  joindm  18008  meetdm  18022  bnj986  32835  satfdm  33231  fmla0  33244  fmlasuc0  33246  dmscut  33932  bj-snsetex  35080  bj-restn0  35188  bj-restuni  35195  ac6s6f  36258  elintima  41150  funressnfv  44424  elpglem2  46303