Theorem spcegv 3512

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543  ∃wex 1787   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-clel 2816

This theorem is referenced by:  spcedv  3513  spcev  3521  eqeu  3619  absneu  4644  issn  4743  elpreqprlem  4776  elunii  4824  axpweq  5257  brcogw  5737  opeldmd  5775  breldmg  5778  dmsnopg  6076  fvrnressn  6976  f1oexbi  7706  unielxp  7799  frrlem13  8039  f1oen3g  8644  f1domg  8648  en2sn  8718  en2snOLD  8719  fodomr  8797  ordiso  9132  fowdom  9187  inf0  9236  infeq5i  9251  oncard  9576  cardsn  9585  dfac8b  9645  ac10ct  9648  aceq3lem  9734  dfacacn  9755  cflem  9860  cflecard  9867  cfslb  9880  coftr  9887  alephsing  9890  fin4i  9912  axdc4lem  10069  gchi  10238  hasheqf1oi  13918  relexpindlem  14626  climeu  15116  brcici  17305  initoeu2lem2  17521  gsumval2a  18157  uptx  22522  alexsubALTlem1  22944  ptcmplem3  22951  prdsxmslem2  23427  tgjustf  26564  tgjustr  26565  wlksnwwlknvbij  27992  clwwlkvbij  28196  aciunf1lem  30719  locfinref  31505  fnimage  33968  fnessref  34283  refssfne  34284  filnetlem4  34307  bj-restb  35000  fin2so  35501  unirep  35608  indexa  35628  rp-isfinite5  40809  nssd  42328  choicefi  42413  axccdom  42435  stoweidlem5  43221  stoweidlem27  43243  stoweidlem28  43244  stoweidlem31  43247  stoweidlem43  43259  stoweidlem44  43260  stoweidlem51  43267  stoweidlem59  43275  nsssmfmbflem  43985  fundcmpsurinjpreimafv  44533  sprbisymrel  44624  isomuspgrlem2  44958  uspgrbisymrelALT  44990  irinitoringc  45300