Theorem isseti 3455

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

Syntax hints:   = wceq 1538  ∃wex 1781   ∈ wcel 2111  Vcvv 3441

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  rexcom4b  3471  ceqsex  3488  vtoclf  3506  vtocl  3507  vtocl2OLD  3510  vtoclef  3531  euind  3663  eusv2nf  5261  zfpair  5287  axprALT  5288  opabn0  5405  isarep2  6413  dfoprab2  7191  rnoprab  7236  ov3  7291  omeu  8194  cflem  9657  genpass  10420  supaddc  11595  supadd  11596  supmul1  11597  supmullem2  11599  supmul  11600  ruclem13  15587  joindm  17605  meetdm  17619  bnj986  32337  satfdm  32729  fmla0  32742  fmlasuc0  32744  dmscut  33385  bj-snsetex  34399  bj-restn0  34505  bj-restuni  34512  ac6s6f  35611  elintima  40354  funressnfv  43635  elpglem2  45241