Theorem isseti 3462

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

Syntax hints:   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803

This theorem is referenced by:  rexcom4b  3476  ceqsal  3482  ceqsalv  3484  ceqsexOLD  3494  ceqsexv2d  3496  vtocle  3518  vtoclOLD  3522  vtoclef  3526  vtoclfOLD  3528  euind  3692  eusv2nf  5345  zfpair  5371  axprALT  5372  opabn0  5508  isarep2  6590  dfoprab2  7427  rnoprab  7474  ov3  7532  omeu  8526  cflem  10174  cflemOLD  10175  genpass  10938  supaddc  12126  supadd  12127  supmul1  12128  supmullem2  12130  supmul  12131  ruclem13  16186  joindm  18314  meetdm  18328  dmscut  27757  bnj986  34938  satfdm  35349  fmla0  35362  fmlasuc0  35364  bj-snsetex  36944  bj-restn0  37071  bj-restuni  37078  ac6s6f  38160  tfsconcatlem  43318  elintima  43635  ormklocald  46865  natlocalincr  46867  tworepnotupword  46877  funressnfv  47037  elpglem2  49694