Theorem spcegv 3581

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-clel 2810

This theorem is referenced by:  spcedv  3582  spcev  3590  eqeu  3694  absneu  4709  issn  4813  elpreqprlem  4847  elunii  4893  axpweq  5326  brcogw  5853  opeldmd  5891  breldmg  5894  dmsnopg  6207  predtrss  6316  fvrnressn  7156  f1oexbi  7929  unielxp  8031  frrlem13  8302  f1oen4g  8984  f1dom4g  8985  f1oen3g  8986  f1dom3g  8987  f1domg  8991  en2sn  9060  en2prd  9067  fodomr  9147  fodomfir  9345  ordiso  9535  fowdom  9590  inf0  9640  infeq5i  9655  oncard  9979  cardsn  9988  dfac8b  10050  ac10ct  10053  aceq3lem  10139  dfacacn  10161  cflem  10264  cflemOLD  10265  cflecard  10272  cfslb  10285  coftr  10292  alephsing  10295  fin4i  10317  axdc4lem  10474  gchi  10643  hasheqf1oi  14374  relexpindlem  15087  climeu  15576  brcici  17818  initoeu2lem2  18033  gsumval2a  18668  irinitoringc  21445  uptx  23568  alexsubALTlem1  23990  ptcmplem3  23997  prdsxmslem2  24473  tgjustf  28457  tgjustr  28458  wlksnwwlknvbij  29895  clwwlkvbij  30099  aciunf1lem  32645  locfinref  33877  fnimage  35952  fnessref  36380  refssfne  36381  filnetlem4  36404  bj-restb  37117  fin2so  37636  unirep  37743  indexa  37762  nssd  45096  choicefi  45191  axccdom  45213  stoweidlem5  46001  stoweidlem27  46023  stoweidlem28  46024  stoweidlem31  46027  stoweidlem43  46039  stoweidlem44  46040  stoweidlem51  46047  stoweidlem59  46055  nsssmfmbflem  46774  fundcmpsurinjpreimafv  47389  sprbisymrel  47480  uspgrbisymrelALT  48097