Theorem isseti 3454

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

Syntax hints:   = wceq 1541  ∃wex 1780   ∈ wcel 2111  Vcvv 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806

This theorem is referenced by:  rexcom4b  3468  ceqsal  3474  ceqsalv  3476  ceqsexv2d  3487  vtocle  3508  vtoclOLD  3512  vtoclef  3516  euind  3678  eusv2nf  5331  zfpair  5357  axprALT  5358  opabn0  5491  isarep2  6571  dfoprab2  7404  rnoprab  7451  ov3  7509  omeu  8500  cflem  10136  cflemOLD  10137  genpass  10900  supaddc  12089  supadd  12090  supmul1  12091  supmullem2  12093  supmul  12094  ruclem13  16151  joindm  18279  meetdm  18293  dmscut  27752  bnj986  34967  satfdm  35413  fmla0  35426  fmlasuc0  35428  bj-snsetex  37005  bj-restn0  37132  bj-restuni  37139  ac6s6f  38221  tfsconcatlem  43377  elintima  43694  ormklocald  46920  natlocalincr  46922  funressnfv  47082  elpglem2  49752