Theorem isseti 3490

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

Syntax hints:   = wceq 1542  ∃wex 1782   ∈ wcel 2107  Vcvv 3475

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 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clel 2811

This theorem is referenced by:  rexcom4b  3504  ceqsal  3510  ceqsalv  3512  ceqsexOLD  3525  ceqsexvOLD  3527  vtoclef  3547  vtoclfOLD  3549  vtocl  3550  euind  3721  eusv2nf  5394  zfpair  5420  axprALT  5421  opabn0  5554  isarep2  6640  dfoprab2  7467  rnoprab  7512  ov3  7570  omeu  8585  cflem  10241  genpass  11004  supaddc  12181  supadd  12182  supmul1  12183  supmullem2  12185  supmul  12186  ruclem13  16185  joindm  18328  meetdm  18342  dmscut  27312  bnj986  33966  satfdm  34360  fmla0  34373  fmlasuc0  34375  bj-snsetex  35844  bj-restn0  35971  bj-restuni  35978  ac6s6f  37041  tfsconcatlem  42086  elintima  42404  natlocalincr  45590  tworepnotupword  45600  funressnfv  45753  elpglem2  47757