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

This proof depends on syntax axioms:   = wceq 1570  ∃wex 1812   ∈ wcel 2147  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2839

This theorem is used by:  rexcom4b  3485  ceqsal  3491  ceqsalv  3493  ceqsexv2d  3503  vtocle  3522  vtoclef  3528  euind  3685  eusv2nf  5364  zfpair  5390  axprALT  5391  opabn0  5535  isarep2  6659  dfoprab2  7509  rnoprab  7556  ov3  7615  omeu  8631  cflem  10362  genpass  11133  supaddc  12324  supadd  12325  supmul1  12326  supmullem2  12328  supmul  12329  ruclem13  16454  joindm  18597  meetdm  18611  dmcuts  28234  bnj986  35696  satfdm  36342  fmla0  36355  fmlasuc0  36357  mirimanoffr  36668  tz9.1tco  37486  bj-snsetex  38091  bj-restn0  38281  bj-restuni  38288  ac6s6f  39371  dmsucmap  39666  tfsconcatlem  44599  elintima  44914  ormklocald  48159  funressnfv  48386  elpglem2  51211