Theorem spcegv 3552

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-clel 2812

This theorem is referenced by:  spcedv  3553  spcev  3561  eqeu  3665  absneu  4686  issn  4789  elpreqprlem  4823  elunii  4869  axpweq  5297  brcogw  5818  opeldmd  5856  breldmg  5859  dmsnopg  6172  predtrss  6281  fvrnressn  7108  f1oexbi  7872  unielxp  7973  frrlem13  8242  f1oen4g  8905  f1dom4g  8906  f1oen3g  8907  f1dom3g  8908  f1domg  8912  en2sn  8982  en2prd  8988  fodomr  9060  fodomfir  9232  ordiso  9425  fowdom  9480  inf0  9534  infeq5i  9549  oncard  9876  cardsn  9885  dfac8b  9945  ac10ct  9948  aceq3lem  10034  dfacacn  10056  cflem  10159  cflemOLD  10160  cflecard  10167  cfslb  10180  coftr  10187  alephsing  10190  fin4i  10212  axdc4lem  10369  gchi  10539  hasheqf1oi  14278  relexpindlem  14990  climeu  15482  brcici  17728  initoeu2lem2  17943  gsumval2a  18614  irinitoringc  21438  uptx  23573  alexsubALTlem1  23995  ptcmplem3  24002  prdsxmslem2  24477  tgjustf  28549  tgjustr  28550  wlksnwwlknvbij  29985  clwwlkvbij  30192  aciunf1lem  32743  locfinref  34000  tz9.1regs  35292  fnimage  36123  fnessref  36553  refssfne  36554  filnetlem4  36577  bj-restb  37301  fin2so  37810  unirep  37917  indexa  37936  nssd  45416  choicefi  45511  axccdom  45533  stoweidlem5  46316  stoweidlem27  46338  stoweidlem28  46339  stoweidlem31  46342  stoweidlem43  46354  stoweidlem44  46355  stoweidlem51  46362  stoweidlem59  46370  nsssmfmbflem  47089  fundcmpsurinjpreimafv  47721  sprbisymrel  47812  uspgrbisymrelALT  48468