Theorem isseti 3456

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 1541  ∃wex 1780   ∈ wcel 2113  Vcvv 3438

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 2809

This theorem is referenced by:  rexcom4b  3470  ceqsal  3476  ceqsalv  3478  ceqsexv2d  3489  vtocle  3510  vtoclOLD  3514  vtoclef  3518  euind  3680  eusv2nf  5338  zfpair  5364  axprALT  5365  opabn0  5499  isarep2  6580  dfoprab2  7414  rnoprab  7461  ov3  7519  omeu  8510  cflem  10153  cflemOLD  10154  genpass  10918  supaddc  12107  supadd  12108  supmul1  12109  supmullem2  12111  supmul  12112  ruclem13  16165  joindm  18294  meetdm  18308  dmscut  27779  bnj986  35060  satfdm  35512  fmla0  35525  fmlasuc0  35527  bj-snsetex  37107  bj-restn0  37234  bj-restuni  37241  ac6s6f  38313  dmsucmap  38581  tfsconcatlem  43520  elintima  43836  ormklocald  47060  natlocalincr  47062  funressnfv  47231  elpglem2  49899