Theorem spcegv 3588

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2138, ax-11 2155. (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 2816	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		spcgv.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	biimprcd 249	. . 3 ⊢ (𝜓 → (𝑥 = 𝐴 → 𝜑))
4	3	eximdv 1921	. 2 ⊢ (𝜓 → (∃𝑥 𝑥 = 𝐴 → ∃𝑥𝜑))
5	1, 4	syl5com 31	1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ∃wex 1782   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-clel 2811

This theorem is referenced by:  spcedv  3589  spcev  3597  eqeu  3703  absneu  4733  issn  4834  elpreqprlem  4867  elunii  4914  axpweq  5349  brcogw  5869  opeldmd  5907  breldmg  5910  dmsnopg  6213  predtrss  6324  fvrnressn  7159  f1oexbi  7919  unielxp  8013  frrlem13  8283  f1oen4g  8960  f1dom4g  8961  f1oen3g  8962  f1dom3g  8963  f1domg  8968  en2sn  9041  en2snOLD  9042  en2prd  9048  fodomr  9128  ordiso  9511  fowdom  9566  inf0  9616  infeq5i  9631  oncard  9955  cardsn  9964  dfac8b  10026  ac10ct  10029  aceq3lem  10115  dfacacn  10136  cflem  10241  cflecard  10248  cfslb  10261  coftr  10268  alephsing  10271  fin4i  10293  axdc4lem  10450  gchi  10619  hasheqf1oi  14311  relexpindlem  15010  climeu  15499  brcici  17747  initoeu2lem2  17965  gsumval2a  18604  uptx  23129  alexsubALTlem1  23551  ptcmplem3  23558  prdsxmslem2  24038  tgjustf  27724  tgjustr  27725  wlksnwwlknvbij  29162  clwwlkvbij  29366  aciunf1lem  31887  locfinref  32821  fnimage  34901  fnessref  35242  refssfne  35243  filnetlem4  35266  bj-restb  35975  fin2so  36475  unirep  36582  indexa  36601  nssd  43794  choicefi  43899  axccdom  43921  stoweidlem5  44721  stoweidlem27  44743  stoweidlem28  44744  stoweidlem31  44747  stoweidlem43  44759  stoweidlem44  44760  stoweidlem51  44767  stoweidlem59  44775  nsssmfmbflem  45494  fundcmpsurinjpreimafv  46076  sprbisymrel  46167  isomuspgrlem2  46501  uspgrbisymrelALT  46533  irinitoringc  46967