Theorem isseti 3458

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

Syntax hints:   = wceq 1541  ∃wex 1780   ∈ wcel 2113  Vcvv 3440

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 2115

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

This theorem is referenced by:  rexcom4b  3472  ceqsal  3478  ceqsalv  3480  ceqsexv2d  3491  vtocle  3512  vtoclOLD  3516  vtoclef  3520  euind  3682  eusv2nf  5340  zfpair  5366  axprALT  5367  opabn0  5501  isarep2  6582  dfoprab2  7416  rnoprab  7463  ov3  7521  omeu  8512  cflem  10155  cflemOLD  10156  genpass  10920  supaddc  12109  supadd  12110  supmul1  12111  supmullem2  12113  supmul  12114  ruclem13  16167  joindm  18296  meetdm  18310  dmcuts  27787  bnj986  35111  satfdm  35563  fmla0  35576  fmlasuc0  35578  bj-snsetex  37164  bj-restn0  37295  bj-restuni  37302  ac6s6f  38374  dmsucmap  38642  tfsconcatlem  43578  elintima  43894  ormklocald  47118  natlocalincr  47120  funressnfv  47289  elpglem2  49957