Theorem isseti 3423

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

Syntax hints:   = wceq 1507  ∃wex 1742   ∈ wcel 2048  Vcvv 3409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765  df-clel 2840

This theorem is referenced by:  rexcom4b  3439  ceqsex  3455  vtoclf  3471  vtocl  3472  vtocl2OLD  3475  vtoclef  3496  euind  3623  eusv2nf  5143  zfpair  5172  axprALT  5173  opabn0  5285  isarep2  6270  dfoprab2  7025  rnoprab  7067  ov3  7121  omeu  8004  cflem  9458  genpass  10221  supaddc  11401  supadd  11402  supmul1  11403  supmullem2  11405  supmul  11406  ruclem13  15445  joindm  17461  meetdm  17475  bnj986  31834  dmscut  32733  bj-snsetex  33728  bj-restn0  33826  bj-restuni  33833  ac6s6f  34843  elintima  39306  funressnfv  42629  elpglem2  44121