Theorem spcegv 3540

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2147, ax-11 2163. (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 2819	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		spcgv.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	biimprcd 250	. . 3 ⊢ (𝜓 → (𝑥 = 𝐴 → 𝜑))
4	3	eximdv 1919	. 2 ⊢ (𝜓 → (∃𝑥 𝑥 = 𝐴 → ∃𝑥𝜑))
5	1, 4	syl5com 31	1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114

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-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-clel 2812

This theorem is referenced by:  spcedv  3541  spcev  3549  eqeu  3653  absneu  4673  issn  4776  elpreqprlem  4810  elunii  4856  axpweq  5289  brcogw  5819  opeldmd  5857  breldmg  5860  dmsnopg  6173  predtrss  6282  fvrnressn  7110  f1oexbi  7874  unielxp  7975  frrlem13  8243  f1oen4g  8906  f1dom4g  8907  f1oen3g  8908  f1dom3g  8909  f1domg  8913  en2sn  8983  en2prd  8989  fodomr  9061  fodomfir  9233  ordiso  9426  fowdom  9481  inf0  9537  infeq5i  9552  oncard  9879  cardsn  9888  dfac8b  9948  ac10ct  9951  aceq3lem  10037  dfacacn  10059  cflem  10162  cflemOLD  10163  cflecard  10170  cfslb  10183  coftr  10190  alephsing  10193  fin4i  10215  axdc4lem  10372  gchi  10542  hasheqf1oi  14308  relexpindlem  15020  climeu  15512  brcici  17762  initoeu2lem2  17977  gsumval2a  18648  irinitoringc  21473  uptx  23604  alexsubALTlem1  24026  ptcmplem3  24033  prdsxmslem2  24508  tgjustf  28559  tgjustr  28560  wlksnwwlknvbij  29995  clwwlkvbij  30202  aciunf1lem  32754  locfinref  34005  tz9.1regs  35298  fnimage  36129  fnessref  36559  refssfne  36560  filnetlem4  36583  dfttc3gw  36725  bj-restb  37426  fin2so  37946  unirep  38053  indexa  38072  nssd  45557  choicefi  45651  axccdom  45673  stoweidlem5  46455  stoweidlem27  46477  stoweidlem28  46478  stoweidlem31  46481  stoweidlem43  46493  stoweidlem44  46494  stoweidlem51  46501  stoweidlem59  46509  nsssmfmbflem  47228  fundcmpsurinjpreimafv  47884  sprbisymrel  47975  uspgrbisymrelALT  48647