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  3720  eusv2nf  5393  zfpair  5419  axprALT  5420  opabn0  5553  isarep2  6637  dfoprab2  7464  rnoprab  7509  ov3  7567  omeu  8582  cflem  10238  genpass  11001  supaddc  12178  supadd  12179  supmul1  12180  supmullem2  12182  supmul  12183  ruclem13  16182  joindm  18325  meetdm  18339  dmscut  27302  bnj986  33955  satfdm  34349  fmla0  34362  fmlasuc0  34364  bj-snsetex  35833  bj-restn0  35960  bj-restuni  35967  ac6s6f  37030  tfsconcatlem  42072  elintima  42390  natlocalincr  45577  tworepnotupword  45587  funressnfv  45740  elpglem2  47711