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  5906  unielxp  6336  op1steq  6341  tfr0dm  6487  tfrlemibxssdm  6492  tfrlemiex  6496  tfr1onlembxssdm  6508  tfr1onlemex  6512  tfrcllembxssdm  6521  tfrcllemex  6525  frecabcl  6564  ertr  6716  f1oen4g  6924  f1dom4g  6925  f1oen3g  6926  f1dom2g  6928  f1domg  6930  dom3d  6946  en1  6972  en2  6997  phpelm  7052  isinfinf  7085  ordiso  7234  djudom  7291  difinfsn  7298  ctm  7307  enumct  7313  djudoml  7433  djudomr  7434  cc2lem  7484  recexnq  7609  ltexprlemrl  7829  ltexprlemru  7831  recexprlemm  7843  recexprlemloc  7850  recexprlem1ssl  7852  recexprlem1ssu  7853  axpre-suploclemres  8120  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  fihasheqf1oi  11048  zfz1isolem1  11103  climeu  11856  fsum3  11947  uzwodc  12607  gsumfzval  13473  mplsubgfilemm  14711  eltg3  14780  uptx  14997  xblm  15140  2lgslem1  15819  upgrex  15953  vtxdumgrfival  16148  1loopgrvd2fi  16155  bj-2inf  16533  subctctexmid  16601