Theorem spcegv 3610

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ∃wex 1777   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-clel 2819

This theorem is referenced by:  spcedv  3611  spcev  3619  eqeu  3728  absneu  4753  issn  4857  elpreqprlem  4890  elunii  4936  axpweq  5369  brcogw  5893  opeldmd  5931  breldmg  5934  dmsnopg  6244  predtrss  6354  fvrnressn  7195  f1oexbi  7968  unielxp  8068  frrlem13  8339  f1oen4g  9024  f1dom4g  9025  f1oen3g  9026  f1dom3g  9027  f1domg  9032  en2sn  9106  en2snOLD  9107  en2prd  9114  fodomr  9194  fodomfir  9396  ordiso  9585  fowdom  9640  inf0  9690  infeq5i  9705  oncard  10029  cardsn  10038  dfac8b  10100  ac10ct  10103  aceq3lem  10189  dfacacn  10211  cflem  10314  cflemOLD  10315  cflecard  10322  cfslb  10335  coftr  10342  alephsing  10345  fin4i  10367  axdc4lem  10524  gchi  10693  hasheqf1oi  14400  relexpindlem  15112  climeu  15601  brcici  17861  initoeu2lem2  18082  gsumval2a  18723  irinitoringc  21513  uptx  23654  alexsubALTlem1  24076  ptcmplem3  24083  prdsxmslem2  24563  tgjustf  28499  tgjustr  28500  wlksnwwlknvbij  29941  clwwlkvbij  30145  aciunf1lem  32680  locfinref  33787  fnimage  35893  fnessref  36323  refssfne  36324  filnetlem4  36347  bj-restb  37060  fin2so  37567  unirep  37674  indexa  37693  nssd  45007  choicefi  45107  axccdom  45129  stoweidlem5  45926  stoweidlem27  45948  stoweidlem28  45949  stoweidlem31  45952  stoweidlem43  45964  stoweidlem44  45965  stoweidlem51  45972  stoweidlem59  45980  nsssmfmbflem  46699  fundcmpsurinjpreimafv  47282  sprbisymrel  47373  uspgrbisymrelALT  47878