Theorem spcegv 3526

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2139, ax-11 2156. (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 2820	. 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 1539  ∃wex 1783   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-clel 2817

This theorem is referenced by:  spcedv  3527  spcev  3535  eqeu  3636  absneu  4661  issn  4760  elpreqprlem  4793  elunii  4841  axpweq  5282  brcogw  5766  opeldmd  5804  breldmg  5807  dmsnopg  6105  predtrss  6214  fvrnressn  7015  f1oexbi  7749  unielxp  7842  frrlem13  8085  f1oen3g  8709  f1dom3g  8710  f1domg  8715  en2sn  8785  en2snOLD  8786  fodomr  8864  ordiso  9205  fowdom  9260  inf0  9309  infeq5i  9324  oncard  9649  cardsn  9658  dfac8b  9718  ac10ct  9721  aceq3lem  9807  dfacacn  9828  cflem  9933  cflecard  9940  cfslb  9953  coftr  9960  alephsing  9963  fin4i  9985  axdc4lem  10142  gchi  10311  hasheqf1oi  13994  relexpindlem  14702  climeu  15192  brcici  17429  initoeu2lem2  17646  gsumval2a  18284  uptx  22684  alexsubALTlem1  23106  ptcmplem3  23113  prdsxmslem2  23591  tgjustf  26738  tgjustr  26739  wlksnwwlknvbij  28174  clwwlkvbij  28378  aciunf1lem  30901  locfinref  31693  fnimage  34158  fnessref  34473  refssfne  34474  filnetlem4  34497  bj-restb  35192  fin2so  35691  unirep  35798  indexa  35818  rp-isfinite5  41022  nssd  42544  choicefi  42629  axccdom  42651  stoweidlem5  43436  stoweidlem27  43458  stoweidlem28  43459  stoweidlem31  43462  stoweidlem43  43474  stoweidlem44  43475  stoweidlem51  43482  stoweidlem59  43490  nsssmfmbflem  44200  fundcmpsurinjpreimafv  44748  sprbisymrel  44839  isomuspgrlem2  45173  uspgrbisymrelALT  45205  irinitoringc  45515