Theorem isseti 3475

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

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

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 2148

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

This theorem is used by:  rexcom4b  3488  ceqsal  3494  ceqsalv  3496  ceqsexv2d  3506  vtocle  3525  vtoclef  3531  euind  3689  eusv2nf  5368  zfpair  5394  axprALT  5395  opabn0  5540  isarep2  6629  dfoprab2  7477  rnoprab  7524  ov3  7582  omeu  8576  cflem  10244  genpass  11009  supaddc  12197  supadd  12198  supmul1  12199  supmullem2  12201  supmul  12202  ruclem13  16320  joindm  18451  meetdm  18465  dmcuts  28035  bnj986  35408  satfdm  35898  fmla0  35911  fmlasuc0  35913  tz9.1tco  37051  bj-snsetex  37656  bj-restn0  37789  bj-restuni  37796  ac6s6f  38880  dmsucmap  39175  tfsconcatlem  44121  elintima  44437  ormklocald  47648  natlocalincr  47650  funressnfv  47838  elpglem2  50547