Theorem isseti 3510

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

Syntax hints:   = wceq 1537  ∃wex 1780   ∈ wcel 2114  Vcvv 3496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895

This theorem is referenced by:  rexcom4b  3526  ceqsex  3542  vtoclf  3560  vtocl  3561  vtocl2OLD  3564  vtoclef  3585  euind  3717  eusv2nf  5298  zfpair  5324  axprALT  5325  opabn0  5442  isarep2  6445  dfoprab2  7214  rnoprab  7259  ov3  7313  omeu  8213  cflem  9670  genpass  10433  supaddc  11610  supadd  11611  supmul1  11612  supmullem2  11614  supmul  11615  ruclem13  15597  joindm  17615  meetdm  17629  bnj986  32229  satfdm  32618  fmla0  32631  fmlasuc0  32633  dmscut  33274  bj-snsetex  34277  bj-restn0  34383  bj-restuni  34390  ac6s6f  35453  elintima  40005  funressnfv  43285  elpglem2  44821