Theorem spcegv 3563

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  3564  spcev  3572  eqeu  3677  absneu  4692  issn  4796  elpreqprlem  4830  elunii  4876  axpweq  5306  brcogw  5832  opeldmd  5870  breldmg  5873  dmsnopg  6186  predtrss  6295  fvrnressn  7133  f1oexbi  7904  unielxp  8006  frrlem13  8277  f1oen4g  8936  f1dom4g  8937  f1oen3g  8938  f1dom3g  8939  f1domg  8943  en2sn  9012  en2prd  9019  fodomr  9092  fodomfir  9279  ordiso  9469  fowdom  9524  inf0  9574  infeq5i  9589  oncard  9913  cardsn  9922  dfac8b  9984  ac10ct  9987  aceq3lem  10073  dfacacn  10095  cflem  10198  cflemOLD  10199  cflecard  10206  cfslb  10219  coftr  10226  alephsing  10229  fin4i  10251  axdc4lem  10408  gchi  10577  hasheqf1oi  14316  relexpindlem  15029  climeu  15521  brcici  17762  initoeu2lem2  17977  gsumval2a  18612  irinitoringc  21389  uptx  23512  alexsubALTlem1  23934  ptcmplem3  23941  prdsxmslem2  24417  tgjustf  28400  tgjustr  28401  wlksnwwlknvbij  29838  clwwlkvbij  30042  aciunf1lem  32586  locfinref  33831  fnimage  35917  fnessref  36345  refssfne  36346  filnetlem4  36369  bj-restb  37082  fin2so  37601  unirep  37708  indexa  37727  nssd  45099  choicefi  45194  axccdom  45216  stoweidlem5  46003  stoweidlem27  46025  stoweidlem28  46026  stoweidlem31  46029  stoweidlem43  46041  stoweidlem44  46042  stoweidlem51  46049  stoweidlem59  46057  nsssmfmbflem  46776  fundcmpsurinjpreimafv  47409  sprbisymrel  47500  uspgrbisymrelALT  48143