Theorem isseti 3469

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

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

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 2836

This theorem is used by:  rexcom4b  3482  ceqsal  3488  ceqsalv  3490  ceqsexv2d  3500  vtocle  3519  vtoclef  3525  euind  3682  eusv2nf  5357  zfpair  5383  axprALT  5384  opabn0  5528  isarep2  6627  dfoprab2  7476  rnoprab  7523  ov3  7581  omeu  8586  cflem  10316  genpass  11087  supaddc  12277  supadd  12278  supmul1  12279  supmullem2  12281  supmul  12282  ruclem13  16403  joindm  18540  meetdm  18554  dmcuts  28170  bnj986  35578  satfdm  36113  fmla0  36126  fmlasuc0  36128  tz9.1tco  37251  bj-snsetex  37856  bj-restn0  37991  bj-restuni  37998  ac6s6f  39085  dmsucmap  39380  tfsconcatlem  44322  elintima  44638  ormklocald  47855  funressnfv  48082  elpglem2  50774