Theorem isseti 3488

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

Syntax hints:   = wceq 1541  ∃wex 1781   ∈ wcel 2106  Vcvv 3473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-clel 2809

This theorem is referenced by:  rexcom4b  3502  ceqsal  3507  ceqsalv  3509  ceqsexOLD  3521  ceqsexvOLD  3523  vtoclef  3543  vtoclfOLD  3545  vtocl  3546  euind  3716  eusv2nf  5386  zfpair  5412  axprALT  5413  opabn0  5546  isarep2  6628  dfoprab2  7451  rnoprab  7496  ov3  7553  omeu  8568  cflem  10223  genpass  10986  supaddc  12163  supadd  12164  supmul1  12165  supmullem2  12167  supmul  12168  ruclem13  16167  joindm  18310  meetdm  18324  dmscut  27238  bnj986  33795  satfdm  34189  fmla0  34202  fmlasuc0  34204  bj-snsetex  35646  bj-restn0  35773  bj-restuni  35780  ac6s6f  36844  tfsconcatlem  41855  elintima  42173  natlocalincr  45361  tworepnotupword  45371  funressnfv  45523  elpglem2  47403