Theorem isseti 3506

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

Syntax hints:   = wceq 1537  ∃wex 1777   ∈ wcel 2108  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819

This theorem is referenced by:  rexcom4b  3521  ceqsal  3527  ceqsalv  3529  ceqsexOLD  3541  ceqsexvOLD  3543  ceqsexv2d  3545  vtocle  3567  vtoclOLD  3571  vtoclef  3575  vtoclfOLD  3577  euind  3746  eusv2nf  5413  zfpair  5439  axprALT  5440  opabn0  5572  isarep2  6669  dfoprab2  7508  rnoprab  7554  ov3  7613  omeu  8641  cflem  10314  cflemOLD  10315  genpass  11078  supaddc  12262  supadd  12263  supmul1  12264  supmullem2  12266  supmul  12267  ruclem13  16290  joindm  18445  meetdm  18459  dmscut  27874  bnj986  34931  satfdm  35337  fmla0  35350  fmlasuc0  35352  bj-snsetex  36929  bj-restn0  37056  bj-restuni  37063  ac6s6f  38133  tfsconcatlem  43298  elintima  43615  natlocalincr  46795  tworepnotupword  46805  funressnfv  46958  elpglem2  48804