Theorem spcegv 2905

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 2384	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1577	. 2 ⊢ Ⅎ𝑥𝜓
3		spcgv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	1, 2, 3	spcegf 2900	1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398  ∃wex 1541   ∈ wcel 2203

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815

This theorem is referenced by:  spcedv  2906  spcev  2912  elabd  2962  eqeu  2987  absneu  3763  elunii  3919  axpweq  4284  euotd  4371  brcogw  4924  opeldmg  4961  breldmg  4962  dmsnopg  5234  dff3im  5822  elunirn  5939  unielxp  6368  op1steq  6373  tfr0dm  6553  tfrlemibxssdm  6558  tfrlemiex  6562  tfr1onlembxssdm  6574  tfr1onlemex  6578  tfrcllembxssdm  6587  tfrcllemex  6591  frecabcl  6630  ertr  6782  f1oen4g  6991  f1dom4g  6992  f1oen3g  6993  f1dom2g  6995  f1domg  6997  dom3d  7013  en1  7039  en2  7065  phpelm  7121  isinfinf  7154  ordiso  7327  djudom  7384  difinfsn  7391  ctm  7400  enumct  7406  djudoml  7526  djudomr  7527  cc2lem  7580  recexnq  7705  ltexprlemrl  7925  ltexprlemru  7927  recexprlemm  7939  recexprlemloc  7946  recexprlem1ssl  7948  recexprlem1ssu  7949  axpre-suploclemres  8216  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  fihasheqf1oi  11150  zfz1isolem1  11212  climeu  11981  fsum3  12073  uzwodc  12733  gsumfzval  13604  mplsubgfilemm  14853  eltg3  14922  uptx  15139  xblm  15282  2lgslem1  15964  upgrex  16098  vtxdumgrfival  16293  1loopgrvd2fi  16300  bj-2inf  16708  subctctexmid  16774