Theorem isseti 3447

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 1782   ∈ wcel 2106  Vcvv 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-clel 2816

This theorem is referenced by:  rexcom4b  3461  ceqsalv  3467  ceqsex  3478  ceqsexv  3479  vtoclf  3497  vtocl  3498  vtoclef  3523  euind  3659  eusv2nf  5318  zfpair  5344  axprALT  5345  opabn0  5466  isarep2  6523  dfoprab2  7333  rnoprab  7378  ov3  7435  omeu  8416  cflem  10002  genpass  10765  supaddc  11942  supadd  11943  supmul1  11944  supmullem2  11946  supmul  11947  ruclem13  15951  joindm  18093  meetdm  18107  bnj986  32935  satfdm  33331  fmla0  33344  fmlasuc0  33346  dmscut  34005  bj-snsetex  35153  bj-restn0  35261  bj-restuni  35268  ac6s6f  36331  elintima  41261  funressnfv  44537  elpglem2  46417  natlocalincr  46511  tworepnotupword  46521