Theorem isseti 3477

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 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3459

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 2809

This theorem is referenced by:  rexcom4b  3492  ceqsal  3498  ceqsalv  3500  ceqsexOLD  3510  ceqsexv2d  3512  vtocle  3534  vtoclOLD  3538  vtoclef  3542  vtoclfOLD  3544  euind  3707  eusv2nf  5365  zfpair  5391  axprALT  5392  opabn0  5528  isarep2  6628  dfoprab2  7465  rnoprab  7512  ov3  7570  omeu  8597  cflem  10259  cflemOLD  10260  genpass  11023  supaddc  12209  supadd  12210  supmul1  12211  supmullem2  12213  supmul  12214  ruclem13  16260  joindm  18385  meetdm  18399  dmscut  27775  bnj986  34986  satfdm  35391  fmla0  35404  fmlasuc0  35406  bj-snsetex  36981  bj-restn0  37108  bj-restuni  37115  ac6s6f  38197  tfsconcatlem  43360  elintima  43677  ormklocald  46903  natlocalincr  46905  tworepnotupword  46915  funressnfv  47072  elpglem2  49576