Theorem isseti 3481

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

Syntax hints:   = wceq 1567  ∃wex 1806   ∈ wcel 2149  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844

This theorem is referenced by:  rexcom4b  3494  ceqsal  3500  ceqsalv  3502  ceqsexv2d  3512  vtocle  3532  vtoclef  3538  euind  3696  eusv2nf  5367  zfpair  5393  axprALT  5394  opabn0  5539  isarep2  6626  dfoprab2  7469  rnoprab  7516  ov3  7574  omeu  8569  cflem  10227  cflemOLD  10228  genpass  10993  supaddc  12181  supadd  12182  supmul1  12183  supmullem2  12185  supmul  12186  ruclem13  16297  joindm  18428  meetdm  18442  dmcuts  27949  bnj986  35287  satfdm  35759  fmla0  35772  fmlasuc0  35774  tz9.1tco  36882  bj-snsetex  37486  bj-restn0  37619  bj-restuni  37626  ac6s6f  38711  dmsucmap  39006  tfsconcatlem  43954  elintima  44270  ormklocald  47481  natlocalincr  47483  funressnfv  47668  elpglem2  50374