Theorem spcegv 3566

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 2811	. 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 2709  df-clel 2804

This theorem is referenced by:  spcedv  3567  spcev  3575  eqeu  3680  absneu  4695  issn  4799  elpreqprlem  4833  elunii  4879  axpweq  5309  brcogw  5835  opeldmd  5873  breldmg  5876  dmsnopg  6189  predtrss  6298  fvrnressn  7136  f1oexbi  7907  unielxp  8009  frrlem13  8280  f1oen4g  8939  f1dom4g  8940  f1oen3g  8941  f1dom3g  8942  f1domg  8946  en2sn  9015  en2prd  9022  fodomr  9098  fodomfir  9286  ordiso  9476  fowdom  9531  inf0  9581  infeq5i  9596  oncard  9920  cardsn  9929  dfac8b  9991  ac10ct  9994  aceq3lem  10080  dfacacn  10102  cflem  10205  cflemOLD  10206  cflecard  10213  cfslb  10226  coftr  10233  alephsing  10236  fin4i  10258  axdc4lem  10415  gchi  10584  hasheqf1oi  14323  relexpindlem  15036  climeu  15528  brcici  17769  initoeu2lem2  17984  gsumval2a  18619  irinitoringc  21396  uptx  23519  alexsubALTlem1  23941  ptcmplem3  23948  prdsxmslem2  24424  tgjustf  28407  tgjustr  28408  wlksnwwlknvbij  29845  clwwlkvbij  30049  aciunf1lem  32593  locfinref  33838  fnimage  35924  fnessref  36352  refssfne  36353  filnetlem4  36376  bj-restb  37089  fin2so  37608  unirep  37715  indexa  37734  nssd  45106  choicefi  45201  axccdom  45223  stoweidlem5  46010  stoweidlem27  46032  stoweidlem28  46033  stoweidlem31  46036  stoweidlem43  46048  stoweidlem44  46049  stoweidlem51  46056  stoweidlem59  46064  nsssmfmbflem  46783  fundcmpsurinjpreimafv  47413  sprbisymrel  47504  uspgrbisymrelALT  48147