Theorem isseti 3507

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

Syntax hints:   = wceq 1531  ∃wex 1774   ∈ wcel 2108  Vcvv 3493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-cleq 2812  df-clel 2891

This theorem is referenced by:  rexcom4b  3523  ceqsex  3539  vtoclf  3557  vtocl  3558  vtocl2OLD  3561  vtoclef  3581  euind  3713  eusv2nf  5286  zfpair  5312  axprALT  5313  opabn0  5431  isarep2  6436  dfoprab2  7204  rnoprab  7249  ov3  7303  omeu  8203  cflem  9660  genpass  10423  supaddc  11600  supadd  11601  supmul1  11602  supmullem2  11604  supmul  11605  ruclem13  15587  joindm  17605  meetdm  17619  bnj986  32220  satfdm  32609  fmla0  32622  fmlasuc0  32624  dmscut  33265  bj-snsetex  34268  bj-restn0  34373  bj-restuni  34380  ac6s6f  35443  elintima  39988  funressnfv  43268  elpglem2  44804