Theorem spcegv 3553

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 2819	. 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 2716  df-clel 2812

This theorem is referenced by:  spcedv  3554  spcev  3562  eqeu  3666  absneu  4687  issn  4790  elpreqprlem  4824  elunii  4870  axpweq  5300  brcogw  5827  opeldmd  5865  breldmg  5868  dmsnopg  6181  predtrss  6290  fvrnressn  7118  f1oexbi  7882  unielxp  7983  frrlem13  8252  f1oen4g  8915  f1dom4g  8916  f1oen3g  8917  f1dom3g  8918  f1domg  8922  en2sn  8992  en2prd  8998  fodomr  9070  fodomfir  9242  ordiso  9435  fowdom  9490  inf0  9544  infeq5i  9559  oncard  9886  cardsn  9895  dfac8b  9955  ac10ct  9958  aceq3lem  10044  dfacacn  10066  cflem  10169  cflemOLD  10170  cflecard  10177  cfslb  10190  coftr  10197  alephsing  10200  fin4i  10222  axdc4lem  10379  gchi  10549  hasheqf1oi  14288  relexpindlem  15000  climeu  15492  brcici  17738  initoeu2lem2  17953  gsumval2a  18624  irinitoringc  21451  uptx  23586  alexsubALTlem1  24008  ptcmplem3  24015  prdsxmslem2  24490  tgjustf  28563  tgjustr  28564  wlksnwwlknvbij  29999  clwwlkvbij  30206  aciunf1lem  32758  locfinref  34025  tz9.1regs  35318  fnimage  36149  fnessref  36579  refssfne  36580  filnetlem4  36603  bj-restb  37374  fin2so  37887  unirep  37994  indexa  38013  nssd  45493  choicefi  45587  axccdom  45609  stoweidlem5  46392  stoweidlem27  46414  stoweidlem28  46415  stoweidlem31  46418  stoweidlem43  46430  stoweidlem44  46431  stoweidlem51  46438  stoweidlem59  46446  nsssmfmbflem  47165  fundcmpsurinjpreimafv  47797  sprbisymrel  47888  uspgrbisymrelALT  48544