Theorem isseti 3498

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

Syntax hints:   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3480

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 2007  ax-8 2110

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

This theorem is referenced by:  rexcom4b  3513  ceqsal  3519  ceqsalv  3521  ceqsexOLD  3531  ceqsexv2d  3533  vtocle  3555  vtoclOLD  3559  vtoclef  3563  vtoclfOLD  3565  euind  3730  eusv2nf  5395  zfpair  5421  axprALT  5422  opabn0  5558  isarep2  6658  dfoprab2  7491  rnoprab  7538  ov3  7596  omeu  8623  cflem  10285  cflemOLD  10286  genpass  11049  supaddc  12235  supadd  12236  supmul1  12237  supmullem2  12239  supmul  12240  ruclem13  16278  joindm  18420  meetdm  18434  dmscut  27856  bnj986  34969  satfdm  35374  fmla0  35387  fmlasuc0  35389  bj-snsetex  36964  bj-restn0  37091  bj-restuni  37098  ac6s6f  38180  tfsconcatlem  43349  elintima  43666  ormklocald  46889  natlocalincr  46891  tworepnotupword  46901  funressnfv  47055  elpglem2  49231