Theorem isseti 3495

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

Syntax hints:   = wceq 1536  ∃wex 1775   ∈ wcel 2105  Vcvv 3477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-clel 2813

This theorem is referenced by:  rexcom4b  3510  ceqsal  3516  ceqsalv  3518  ceqsexOLD  3528  ceqsexvOLD  3530  ceqsexv2d  3532  vtocle  3554  vtoclOLD  3558  vtoclef  3562  vtoclfOLD  3564  euind  3732  eusv2nf  5400  zfpair  5426  axprALT  5427  opabn0  5562  isarep2  6658  dfoprab2  7490  rnoprab  7536  ov3  7595  omeu  8621  cflem  10282  cflemOLD  10283  genpass  11046  supaddc  12232  supadd  12233  supmul1  12234  supmullem2  12236  supmul  12237  ruclem13  16274  joindm  18432  meetdm  18446  dmscut  27870  bnj986  34947  satfdm  35353  fmla0  35366  fmlasuc0  35368  bj-snsetex  36945  bj-restn0  37072  bj-restuni  37079  ac6s6f  38159  tfsconcatlem  43325  elintima  43642  natlocalincr  46829  tworepnotupword  46839  funressnfv  46992  elpglem2  48942