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  27313  bnj986  33997  satfdm  34391  fmla0  34404  fmlasuc0  34406  bj-snsetex  35892  bj-restn0  36019  bj-restuni  36026  ac6s6f  37089  tfsconcatlem  42134  elintima  42452  natlocalincr  45638  tworepnotupword  45648  funressnfv  45801  elpglem2  47805