Theorem isseti 3454

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 3436

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  3468  ceqsal  3474  ceqsalv  3476  ceqsexOLD  3486  ceqsexv2d  3488  vtocle  3510  vtoclOLD  3514  vtoclef  3518  vtoclfOLD  3520  euind  3684  eusv2nf  5334  zfpair  5360  axprALT  5361  opabn0  5496  isarep2  6572  dfoprab2  7407  rnoprab  7454  ov3  7512  omeu  8503  cflem  10139  cflemOLD  10140  genpass  10903  supaddc  12092  supadd  12093  supmul1  12094  supmullem2  12096  supmul  12097  ruclem13  16151  joindm  18279  meetdm  18293  dmscut  27722  bnj986  34922  satfdm  35342  fmla0  35355  fmlasuc0  35357  bj-snsetex  36937  bj-restn0  37064  bj-restuni  37071  ac6s6f  38153  tfsconcatlem  43309  elintima  43626  ormklocald  46855  natlocalincr  46857  tworepnotupword  46867  funressnfv  47027  elpglem2  49697