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 ⊢ ∃𝑥 𝑥 = 𝐴

This proof depends on syntax axioms:   = wceq 1569  ∃wex 1808   ∈ wcel 2142  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-clel 2837

This theorem is used by:  rexcom4b  3485  ceqsal  3491  ceqsalv  3493  ceqsexv2d  3503  vtocle  3522  vtoclef  3528  euind  3686  eusv2nf  5365  zfpair  5391  axprALT  5392  opabn0  5537  isarep2  6625  dfoprab2  7470  rnoprab  7517  ov3  7575  omeu  8568  cflem  10235  genpass  11000  supaddc  12188  supadd  12189  supmul1  12190  supmullem2  12192  supmul  12193  ruclem13  16304  joindm  18435  meetdm  18449  dmcuts  27995  bnj986  35352  satfdm  35869  fmla0  35882  fmlasuc0  35884  tz9.1tco  37022  bj-snsetex  37627  bj-restn0  37760  bj-restuni  37767  ac6s6f  38850  dmsucmap  39145  tfsconcatlem  44091  elintima  44407  ormklocald  47618  natlocalincr  47620  funressnfv  47808  elpglem2  50518