Theorem isseti 3465

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 3447

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  3479  ceqsal  3485  ceqsalv  3487  ceqsexOLD  3497  ceqsexv2d  3499  vtocle  3521  vtoclOLD  3525  vtoclef  3529  vtoclfOLD  3531  euind  3695  eusv2nf  5350  zfpair  5376  axprALT  5377  opabn0  5513  isarep2  6608  dfoprab2  7447  rnoprab  7494  ov3  7552  omeu  8549  cflem  10198  cflemOLD  10199  genpass  10962  supaddc  12150  supadd  12151  supmul1  12152  supmullem2  12154  supmul  12155  ruclem13  16210  joindm  18334  meetdm  18348  dmscut  27723  bnj986  34945  satfdm  35356  fmla0  35369  fmlasuc0  35371  bj-snsetex  36951  bj-restn0  37078  bj-restuni  37085  ac6s6f  38167  tfsconcatlem  43325  elintima  43642  ormklocald  46872  natlocalincr  46874  tworepnotupword  46884  funressnfv  47044  elpglem2  49701