Theorem isseti 3473

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

Syntax hints:   = wceq 1570  ∃wex 1809   ∈ wcel 2143  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838

This theorem is referenced by:  rexcom4b  3486  ceqsal  3492  ceqsalv  3494  ceqsexv2d  3504  vtocle  3523  vtoclef  3529  euind  3687  eusv2nf  5366  zfpair  5392  axprALT  5393  opabn0  5538  isarep2  6625  dfoprab2  7468  rnoprab  7515  ov3  7573  omeu  8566  cflem  10224  genpass  10989  supaddc  12177  supadd  12178  supmul1  12179  supmullem2  12181  supmul  12182  ruclem13  16293  joindm  18424  meetdm  18438  dmcuts  27984  bnj986  35343  satfdm  35861  fmla0  35874  fmlasuc0  35876  tz9.1tco  36994  bj-snsetex  37599  bj-restn0  37732  bj-restuni  37739  ac6s6f  38822  dmsucmap  39117  tfsconcatlem  44063  elintima  44379  ormklocald  47590  natlocalincr  47592  funressnfv  47780  elpglem2  50490