Theorem spcegv 3558

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562  ∃wex 1801   ∈ wcel 2144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-clel 2839

This theorem is referenced by:  spcedv  3559  spcev  3567  eqeu  3671  absneu  4689  issn  4792  elpreqprlem  4826  elunii  4872  axpweq  5309  brcogw  5842  opeldmd  5884  breldmg  5887  dmsnopg  6202  predtrss  6311  fvrnressn  7146  f1oexbi  7911  unielxp  8010  frrlem13  8281  f1oen4g  8947  f1dom4g  8948  f1oen3g  8949  f1dom3g  8950  f1domg  8954  en2sn  9024  en2prd  9030  fodomr  9102  fodomfir  9274  ordiso  9466  fowdom  9521  inf0  9578  infeq5i  9593  oncard  9920  cardsn  9929  dfac8b  9989  ac10ct  9992  aceq3lem  10078  dfacacn  10100  cflem  10203  cflemOLD  10204  cflecard  10211  cfslb  10225  coftr  10232  alephsing  10235  fin4i  10257  axdc4lem  10414  gchi  10584  hasheqf1oi  14366  relexpindlem  15078  climeu  15584  brcici  17835  initoeu2lem2  18050  gsumval2a  18721  irinitoringc  21533  uptx  23687  alexsubALTlem1  24109  ptcmplem3  24116  prdsxmslem2  24591  tgjustf  28644  tgjustr  28645  wlksnwwlknvbij  30110  clwwlkvbij  30317  aciunf1lem  32866  locfinref  34140  tz9.1regs  35434  fnimage  36282  fnessref  36722  refssfne  36723  filnetlem4  36746  dfttc3gw  36888  bj-restb  37589  fin2so  38111  unirep  38218  indexa  38237  nssd  45688  choicefi  45782  axccdom  45803  stoweidlem5  46584  stoweidlem27  46606  stoweidlem28  46607  stoweidlem31  46610  stoweidlem43  46622  stoweidlem44  46623  stoweidlem51  46630  stoweidlem59  46638  nsssmfmbflem  47357  fundcmpsurinjpreimafv  48019  sprbisymrel  48110  uspgrbisymrelALT  48782