Theorem isseti 3460

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

Syntax hints:   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812

This theorem is referenced by:  rexcom4b  3474  ceqsal  3480  ceqsalv  3482  ceqsexv2d  3493  vtocle  3514  vtoclOLD  3518  vtoclef  3522  euind  3684  eusv2nf  5342  zfpair  5368  axprALT  5369  opabn0  5509  isarep2  6590  dfoprab2  7426  rnoprab  7473  ov3  7531  omeu  8522  cflem  10167  cflemOLD  10168  genpass  10932  supaddc  12121  supadd  12122  supmul1  12123  supmullem2  12125  supmul  12126  ruclem13  16179  joindm  18308  meetdm  18322  dmcuts  27799  bnj986  35131  satfdm  35585  fmla0  35598  fmlasuc0  35600  bj-snsetex  37211  bj-restn0  37343  bj-restuni  37350  ac6s6f  38424  dmsucmap  38719  tfsconcatlem  43693  elintima  44009  ormklocald  47232  natlocalincr  47234  funressnfv  47403  elpglem2  50071