Theorem isseti 3448

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

Syntax hints:   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812

This theorem is referenced by:  rexcom4b  3462  ceqsal  3468  ceqsalv  3470  ceqsexv2d  3480  vtocle  3501  vtoclOLD  3505  vtoclef  3509  euind  3671  eusv2nf  5333  zfpair  5359  axprALT  5360  opabn0  5502  isarep2  6583  dfoprab2  7419  rnoprab  7466  ov3  7524  omeu  8514  cflem  10161  cflemOLD  10162  genpass  10926  supaddc  12117  supadd  12118  supmul1  12119  supmullem2  12121  supmul  12122  ruclem13  16203  joindm  18333  meetdm  18347  dmcuts  27800  bnj986  35116  satfdm  35570  fmla0  35583  fmlasuc0  35585  tz9.1tco  36684  bj-snsetex  37289  bj-restn0  37421  bj-restuni  37428  ac6s6f  38511  dmsucmap  38806  tfsconcatlem  43785  elintima  44101  ormklocald  47323  natlocalincr  47325  funressnfv  47506  elpglem2  50202