Theorem spcegv 3539

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 2818	. 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 2715  df-clel 2811

This theorem is referenced by:  spcedv  3540  spcev  3548  eqeu  3652  absneu  4672  issn  4775  elpreqprlem  4809  elunii  4855  axpweq  5292  brcogw  5823  opeldmd  5861  breldmg  5864  dmsnopg  6177  predtrss  6286  fvrnressn  7115  f1oexbi  7879  unielxp  7980  frrlem13  8248  f1oen4g  8911  f1dom4g  8912  f1oen3g  8913  f1dom3g  8914  f1domg  8918  en2sn  8988  en2prd  8994  fodomr  9066  fodomfir  9238  ordiso  9431  fowdom  9486  inf0  9542  infeq5i  9557  oncard  9884  cardsn  9893  dfac8b  9953  ac10ct  9956  aceq3lem  10042  dfacacn  10064  cflem  10167  cflemOLD  10168  cflecard  10175  cfslb  10188  coftr  10195  alephsing  10198  fin4i  10220  axdc4lem  10377  gchi  10547  hasheqf1oi  14313  relexpindlem  15025  climeu  15517  brcici  17767  initoeu2lem2  17982  gsumval2a  18653  irinitoringc  21459  uptx  23590  alexsubALTlem1  24012  ptcmplem3  24019  prdsxmslem2  24494  tgjustf  28541  tgjustr  28542  wlksnwwlknvbij  29976  clwwlkvbij  30183  aciunf1lem  32735  locfinref  33985  tz9.1regs  35278  fnimage  36109  fnessref  36539  refssfne  36540  filnetlem4  36563  dfttc3gw  36705  bj-restb  37406  fin2so  37928  unirep  38035  indexa  38054  nssd  45535  choicefi  45629  axccdom  45651  stoweidlem5  46433  stoweidlem27  46455  stoweidlem28  46456  stoweidlem31  46459  stoweidlem43  46471  stoweidlem44  46472  stoweidlem51  46479  stoweidlem59  46487  nsssmfmbflem  47206  fundcmpsurinjpreimafv  47868  sprbisymrel  47959  uspgrbisymrelALT  48631