Theorem spcegv 3549

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2146, ax-11 2162. (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 250	. . 3 ⊢ (𝜓 → (𝑥 = 𝐴 → 𝜑))
4	3	eximdv 1918	. 2 ⊢ (𝜓 → (∃𝑥 𝑥 = 𝐴 → ∃𝑥𝜑))
5	1, 4	syl5com 31	1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-clel 2809

This theorem is referenced by:  spcedv  3550  spcev  3558  eqeu  3662  absneu  4683  issn  4786  elpreqprlem  4820  elunii  4866  axpweq  5294  brcogw  5815  opeldmd  5853  breldmg  5856  dmsnopg  6169  predtrss  6278  fvrnressn  7104  f1oexbi  7868  unielxp  7969  frrlem13  8238  f1oen4g  8899  f1dom4g  8900  f1oen3g  8901  f1dom3g  8902  f1domg  8906  en2sn  8976  en2prd  8982  fodomr  9054  fodomfir  9226  ordiso  9419  fowdom  9474  inf0  9528  infeq5i  9543  oncard  9870  cardsn  9879  dfac8b  9939  ac10ct  9942  aceq3lem  10028  dfacacn  10050  cflem  10153  cflemOLD  10154  cflecard  10161  cfslb  10174  coftr  10181  alephsing  10184  fin4i  10206  axdc4lem  10363  gchi  10533  hasheqf1oi  14272  relexpindlem  14984  climeu  15476  brcici  17722  initoeu2lem2  17937  gsumval2a  18608  irinitoringc  21432  uptx  23567  alexsubALTlem1  23989  ptcmplem3  23996  prdsxmslem2  24471  tgjustf  28494  tgjustr  28495  wlksnwwlknvbij  29930  clwwlkvbij  30137  aciunf1lem  32689  locfinref  33947  tz9.1regs  35239  fnimage  36070  fnessref  36500  refssfne  36501  filnetlem4  36524  bj-restb  37238  fin2so  37747  unirep  37854  indexa  37873  nssd  45291  choicefi  45386  axccdom  45408  stoweidlem5  46191  stoweidlem27  46213  stoweidlem28  46214  stoweidlem31  46217  stoweidlem43  46229  stoweidlem44  46230  stoweidlem51  46237  stoweidlem59  46245  nsssmfmbflem  46964  fundcmpsurinjpreimafv  47596  sprbisymrel  47687  uspgrbisymrelALT  48343