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

Syntax hints:   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2804

This theorem is referenced by:  rexcom4b  3482  ceqsal  3488  ceqsalv  3490  ceqsexOLD  3500  ceqsexv2d  3502  vtocle  3524  vtoclOLD  3528  vtoclef  3532  vtoclfOLD  3534  euind  3698  eusv2nf  5353  zfpair  5379  axprALT  5380  opabn0  5516  isarep2  6611  dfoprab2  7450  rnoprab  7497  ov3  7555  omeu  8552  cflem  10205  cflemOLD  10206  genpass  10969  supaddc  12157  supadd  12158  supmul1  12159  supmullem2  12161  supmul  12162  ruclem13  16217  joindm  18341  meetdm  18355  dmscut  27730  bnj986  34952  satfdm  35363  fmla0  35376  fmlasuc0  35378  bj-snsetex  36958  bj-restn0  37085  bj-restuni  37092  ac6s6f  38174  tfsconcatlem  43332  elintima  43649  ormklocald  46879  natlocalincr  46881  tworepnotupword  46891  funressnfv  47048  elpglem2  49705