Theorem spcegv 3560

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 2810	. 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 2708  df-clel 2803

This theorem is referenced by:  spcedv  3561  spcev  3569  eqeu  3674  absneu  4688  issn  4792  elpreqprlem  4826  elunii  4872  axpweq  5301  brcogw  5822  opeldmd  5860  breldmg  5863  dmsnopg  6174  predtrss  6283  fvrnressn  7115  f1oexbi  7884  unielxp  7985  frrlem13  8254  f1oen4g  8913  f1dom4g  8914  f1oen3g  8915  f1dom3g  8916  f1domg  8920  en2sn  8989  en2prd  8996  fodomr  9069  fodomfir  9255  ordiso  9445  fowdom  9500  inf0  9550  infeq5i  9565  oncard  9889  cardsn  9898  dfac8b  9960  ac10ct  9963  aceq3lem  10049  dfacacn  10071  cflem  10174  cflemOLD  10175  cflecard  10182  cfslb  10195  coftr  10202  alephsing  10205  fin4i  10227  axdc4lem  10384  gchi  10553  hasheqf1oi  14292  relexpindlem  15005  climeu  15497  brcici  17742  initoeu2lem2  17957  gsumval2a  18594  irinitoringc  21421  uptx  23545  alexsubALTlem1  23967  ptcmplem3  23974  prdsxmslem2  24450  tgjustf  28453  tgjustr  28454  wlksnwwlknvbij  29888  clwwlkvbij  30092  aciunf1lem  32636  locfinref  33824  fnimage  35910  fnessref  36338  refssfne  36339  filnetlem4  36362  bj-restb  37075  fin2so  37594  unirep  37701  indexa  37720  nssd  45092  choicefi  45187  axccdom  45209  stoweidlem5  45996  stoweidlem27  46018  stoweidlem28  46019  stoweidlem31  46022  stoweidlem43  46034  stoweidlem44  46035  stoweidlem51  46042  stoweidlem59  46050  nsssmfmbflem  46769  fundcmpsurinjpreimafv  47402  sprbisymrel  47493  uspgrbisymrelALT  48136