Theorem isseti 3449

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

Syntax hints:   = wceq 1547  ∃wex 1786   ∈ wcel 2119  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2814

This theorem is referenced by:  rexcom4b  3462  ceqsal  3468  ceqsalv  3470  ceqsexv2d  3480  vtocle  3501  vtoclOLD  3504  vtoclef  3508  euind  3665  eusv2nf  5324  zfpair  5350  axprALT  5351  opabn0  5495  isarep2  6575  dfoprab2  7414  rnoprab  7461  ov3  7519  omeu  8510  cflem  10158  cflemOLD  10159  genpass  10923  supaddc  12114  supadd  12115  supmul1  12116  supmullem2  12118  supmul  12119  ruclem13  16200  joindm  18330  meetdm  18344  dmcuts  27801  bnj986  35137  satfdm  35597  fmla0  35610  fmlasuc0  35612  tz9.1tco  36711  bj-snsetex  37316  bj-restn0  37448  bj-restuni  37455  ac6s6f  38540  dmsucmap  38835  tfsconcatlem  43781  elintima  44097  ormklocald  47319  natlocalincr  47321  funressnfv  47506  elpglem2  50202