Theorem isseti 3468

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147

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

This theorem is used by:  rexcom4b  3481  ceqsal  3487  ceqsalv  3489  ceqsexv2d  3499  vtocle  3518  vtoclef  3524  euind  3682  eusv2nf  5360  zfpair  5386  axprALT  5387  opabn0  5532  isarep2  6622  dfoprab2  7471  rnoprab  7518  ov3  7576  omeu  8572  cflem  10247  genpass  11018  supaddc  12206  supadd  12207  supmul1  12208  supmullem2  12210  supmul  12211  ruclem13  16330  joindm  18461  meetdm  18475  dmcuts  28056  bnj986  35464  satfdm  35948  fmla0  35961  fmlasuc0  35963  tz9.1tco  37102  bj-snsetex  37707  bj-restn0  37840  bj-restuni  37847  ac6s6f  38921  dmsucmap  39216  tfsconcatlem  44177  elintima  44493  ormklocald  47704  funressnfv  47931  elpglem2  50638