Theorem isseti 3447

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

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

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 2811

This theorem is referenced by:  rexcom4b  3461  ceqsal  3467  ceqsalv  3469  ceqsexv2d  3479  vtocle  3500  vtoclOLD  3504  vtoclef  3508  euind  3670  eusv2nf  5337  zfpair  5363  axprALT  5364  opabn0  5508  isarep2  6588  dfoprab2  7425  rnoprab  7472  ov3  7530  omeu  8520  cflem  10167  cflemOLD  10168  genpass  10932  supaddc  12123  supadd  12124  supmul1  12125  supmullem2  12127  supmul  12128  ruclem13  16209  joindm  18339  meetdm  18353  dmcuts  27783  bnj986  35097  satfdm  35551  fmla0  35564  fmlasuc0  35566  tz9.1tco  36665  bj-snsetex  37270  bj-restn0  37402  bj-restuni  37409  ac6s6f  38494  dmsucmap  38789  tfsconcatlem  43764  elintima  44080  ormklocald  47304  natlocalincr  47306  funressnfv  47491  elpglem2  50187