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  18310  meetdm  18324  dmscut  27699  bnj986  34918  satfdm  35329  fmla0  35342  fmlasuc0  35344  bj-snsetex  36924  bj-restn0  37051  bj-restuni  37058  ac6s6f  38140  tfsconcatlem  43298  elintima  43615  ormklocald  46845  natlocalincr  46847  tworepnotupword  46857  funressnfv  47017  elpglem2  49674