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 1569  ∃wex 1811   ∈ wcel 2144  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

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

This theorem is used by:  rexcom4b  3481  ceqsal  3487  ceqsalv  3489  ceqsexv2d  3499  vtocle  3518  vtoclef  3524  euind  3681  eusv2nf  5357  zfpair  5383  axprALT  5384  opabn0  5528  isarep2  6634  dfoprab2  7482  rnoprab  7529  ov3  7587  omeu  8600  cflem  10330  genpass  11101  supaddc  12291  supadd  12292  supmul1  12293  supmullem2  12295  supmul  12296  ruclem13  16419  joindm  18556  meetdm  18570  dmcuts  28186  bnj986  35635  satfdm  36224  fmla0  36237  fmlasuc0  36239  mirimanoffr  36550  tz9.1tco  37367  bj-snsetex  37972  bj-restn0  38119  bj-restuni  38126  ac6s6f  39214  dmsucmap  39509  tfsconcatlem  44447  elintima  44762  ormklocald  47994  funressnfv  48221  elpglem2  50988