Theorem spcegv 3547

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2144, ax-11 2160. (Revised by Wolf Lammen, 25-Aug-2023.)

Hypothesis

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

Assertion

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

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

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

Proof of Theorem spcegv

Step	Hyp	Ref	Expression
1		elisset 2813	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		spcgv.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	biimprcd 250	. . 3 ⊢ (𝜓 → (𝑥 = 𝐴 → 𝜑))
4	3	eximdv 1918	. 2 ⊢ (𝜓 → (∃𝑥 𝑥 = 𝐴 → ∃𝑥𝜑))
5	1, 4	syl5com 31	1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-clel 2806

This theorem is referenced by:  spcedv  3548  spcev  3556  eqeu  3660  absneu  4678  issn  4781  elpreqprlem  4815  elunii  4861  axpweq  5287  brcogw  5807  opeldmd  5845  breldmg  5848  dmsnopg  6160  predtrss  6269  fvrnressn  7094  f1oexbi  7858  unielxp  7959  frrlem13  8228  f1oen4g  8887  f1dom4g  8888  f1oen3g  8889  f1dom3g  8890  f1domg  8894  en2sn  8963  en2prd  8969  fodomr  9041  fodomfir  9212  ordiso  9402  fowdom  9457  inf0  9511  infeq5i  9526  oncard  9853  cardsn  9862  dfac8b  9922  ac10ct  9925  aceq3lem  10011  dfacacn  10033  cflem  10136  cflemOLD  10137  cflecard  10144  cfslb  10157  coftr  10164  alephsing  10167  fin4i  10189  axdc4lem  10346  gchi  10515  hasheqf1oi  14258  relexpindlem  14970  climeu  15462  brcici  17707  initoeu2lem2  17922  gsumval2a  18593  irinitoringc  21416  uptx  23540  alexsubALTlem1  23962  ptcmplem3  23969  prdsxmslem2  24444  tgjustf  28451  tgjustr  28452  wlksnwwlknvbij  29886  clwwlkvbij  30093  aciunf1lem  32644  locfinref  33854  tz9.1regs  35130  fnimage  35971  fnessref  36401  refssfne  36402  filnetlem4  36425  bj-restb  37138  fin2so  37646  unirep  37753  indexa  37772  nssd  45201  choicefi  45296  axccdom  45318  stoweidlem5  46102  stoweidlem27  46124  stoweidlem28  46125  stoweidlem31  46128  stoweidlem43  46140  stoweidlem44  46141  stoweidlem51  46148  stoweidlem59  46156  nsssmfmbflem  46875  fundcmpsurinjpreimafv  47507  sprbisymrel  47598  uspgrbisymrelALT  48254