Theorem spcegv 3565

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  ∃wex 1806   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-clel 2844

This theorem is referenced by:  spcedv  3566  spcev  3574  eqeu  3678  absneu  4699  issn  4801  elpreqprlem  4835  elunii  4881  axpweq  5322  brcogw  5855  opeldmd  5897  breldmg  5900  dmsnopg  6215  predtrss  6324  fvrnressn  7159  f1oexbi  7925  unielxp  8024  frrlem13  8295  f1oen4g  8961  f1dom4g  8962  f1oen3g  8963  f1dom3g  8964  f1domg  8968  en2sn  9038  en2prd  9044  fodomr  9116  fodomfir  9287  ordiso  9478  fowdom  9533  inf0  9590  infeq5i  9605  oncard  9946  cardsn  9955  dfac8b  10015  ac10ct  10018  aceq3lem  10104  dfacacn  10125  cflem  10228  cflemOLD  10229  cflecard  10236  cfslb  10250  coftr  10257  alephsing  10260  fin4i  10282  axdc4lem  10439  gchi  10609  hasheqf1oi  14387  relexpindlem  15100  climeu  15606  brcici  17857  initoeu2lem2  18072  gsumval2a  18743  irinitoringc  21598  uptx  23751  alexsubALTlem1  24173  ptcmplem3  24180  prdsxmslem2  24655  tgjustf  28708  tgjustr  28709  wlksnwwlknvbij  30198  clwwlkvbij  30405  aciunf1lem  32948  locfinref  34176  tz9.1regs  35480  fnimage  36352  fnessref  36791  refssfne  36792  filnetlem4  36815  dfttc3gw  36957  bj-restb  37658  fin2so  38180  unirep  38287  indexa  38306  nssd  45749  choicefi  45843  axccdom  45864  stoweidlem5  46645  stoweidlem27  46667  stoweidlem28  46668  stoweidlem31  46671  stoweidlem43  46683  stoweidlem44  46684  stoweidlem51  46691  stoweidlem59  46699  nsssmfmbflem  47418  fundcmpsurinjpreimafv  48080  sprbisymrel  48171  uspgrbisymrelALT  48843