Theorem isseti 3472

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

Syntax hints:   = wceq 1560  ∃wex 1799   ∈ wcel 2142  Vcvv 3454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-clel 2837

This theorem is referenced by:  rexcom4b  3485  ceqsal  3491  ceqsalv  3493  ceqsexv2d  3503  vtocle  3523  vtoclef  3529  euind  3687  eusv2nf  5352  zfpair  5378  axprALT  5379  opabn0  5524  isarep2  6611  dfoprab2  7454  rnoprab  7501  ov3  7559  omeu  8554  cflem  10201  cflemOLD  10202  genpass  10967  supaddc  12159  supadd  12160  supmul1  12161  supmullem2  12163  supmul  12164  ruclem13  16274  joindm  18405  meetdm  18419  dmcuts  27881  bnj986  35247  satfdm  35716  fmla0  35729  fmlasuc0  35731  tz9.1tco  36840  bj-snsetex  37445  bj-restn0  37577  bj-restuni  37584  ac6s6f  38669  dmsucmap  38964  tfsconcatlem  43910  elintima  44226  ormklocald  47447  natlocalincr  47449  funressnfv  47634  elpglem2  50330