Theorem spcegv 3596

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2140, ax-11 2156. (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 2822	. 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 1539  ∃wex 1778   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-clel 2815

This theorem is referenced by:  spcedv  3597  spcev  3605  eqeu  3711  absneu  4727  issn  4831  elpreqprlem  4865  elunii  4911  axpweq  5350  brcogw  5878  opeldmd  5916  breldmg  5919  dmsnopg  6232  predtrss  6342  fvrnressn  7180  f1oexbi  7951  unielxp  8053  frrlem13  8324  f1oen4g  9006  f1dom4g  9007  f1oen3g  9008  f1dom3g  9009  f1domg  9013  en2sn  9082  en2prd  9089  fodomr  9169  fodomfir  9369  ordiso  9557  fowdom  9612  inf0  9662  infeq5i  9677  oncard  10001  cardsn  10010  dfac8b  10072  ac10ct  10075  aceq3lem  10161  dfacacn  10183  cflem  10286  cflemOLD  10287  cflecard  10294  cfslb  10307  coftr  10314  alephsing  10317  fin4i  10339  axdc4lem  10496  gchi  10665  hasheqf1oi  14391  relexpindlem  15103  climeu  15592  brcici  17845  initoeu2lem2  18061  gsumval2a  18699  irinitoringc  21491  uptx  23634  alexsubALTlem1  24056  ptcmplem3  24063  prdsxmslem2  24543  tgjustf  28482  tgjustr  28483  wlksnwwlknvbij  29929  clwwlkvbij  30133  aciunf1lem  32673  locfinref  33841  fnimage  35931  fnessref  36359  refssfne  36360  filnetlem4  36383  bj-restb  37096  fin2so  37615  unirep  37722  indexa  37741  nssd  45115  choicefi  45210  axccdom  45232  stoweidlem5  46025  stoweidlem27  46047  stoweidlem28  46048  stoweidlem31  46051  stoweidlem43  46063  stoweidlem44  46064  stoweidlem51  46071  stoweidlem59  46079  nsssmfmbflem  46798  fundcmpsurinjpreimafv  47400  sprbisymrel  47491  uspgrbisymrelALT  48076