Theorem spcegv 2894

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.)

Hypothesis

Ref	Expression
spcgv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
spcegv	⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem spcegv

Step	Hyp	Ref	Expression
1		nfcv 2374	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1576	. 2 ⊢ Ⅎ𝑥𝜓
3		spcgv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	1, 2, 3	spcegf 2889	1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397  ∃wex 1540   ∈ wcel 2202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804

This theorem is referenced by:  spcedv  2895  spcev  2901  elabd  2951  eqeu  2976  absneu  3743  elunii  3898  axpweq  4261  euotd  4347  brcogw  4899  opeldmg  4936  breldmg  4937  dmsnopg  5208  dff3im  5792  elunirn  5907  unielxp  6337  op1steq  6342  tfr0dm  6488  tfrlemibxssdm  6493  tfrlemiex  6497  tfr1onlembxssdm  6509  tfr1onlemex  6513  tfrcllembxssdm  6522  tfrcllemex  6526  frecabcl  6565  ertr  6717  f1oen4g  6925  f1dom4g  6926  f1oen3g  6927  f1dom2g  6929  f1domg  6931  dom3d  6947  en1  6973  en2  6998  phpelm  7053  isinfinf  7086  ordiso  7235  djudom  7292  difinfsn  7299  ctm  7308  enumct  7314  djudoml  7434  djudomr  7435  cc2lem  7485  recexnq  7610  ltexprlemrl  7830  ltexprlemru  7832  recexprlemm  7844  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  axpre-suploclemres  8121  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  fihasheqf1oi  11050  zfz1isolem1  11105  climeu  11874  fsum3  11966  uzwodc  12626  gsumfzval  13492  mplsubgfilemm  14731  eltg3  14800  uptx  15017  xblm  15160  2lgslem1  15839  upgrex  15973  vtxdumgrfival  16168  1loopgrvd2fi  16175  bj-2inf  16584  subctctexmid  16652