Theorem spcegv 3537

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548  ∃wex 1787   ∈ wcel 2121

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 1975  ax-7 2016  ax-8 2123

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-clel 2816

This theorem is referenced by:  spcedv  3538  spcev  3546  eqeu  3649  absneu  4663  issn  4766  elpreqprlem  4800  elunii  4846  axpweq  5282  brcogw  5813  opeldmd  5855  breldmg  5858  dmsnopg  6168  predtrss  6277  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  9537  infeq5i  9552  oncard  9879  cardsn  9888  dfac8b  9948  ac10ct  9951  aceq3lem  10037  dfacacn  10059  cflem  10162  cflemOLD  10163  cflecard  10170  cfslb  10183  coftr  10190  alephsing  10193  fin4i  10215  axdc4lem  10372  gchi  10542  hasheqf1oi  14308  relexpindlem  15020  climeu  15512  brcici  17762  initoeu2lem2  17977  gsumval2a  18648  irinitoringc  21458  uptx  23612  alexsubALTlem1  24034  ptcmplem3  24041  prdsxmslem2  24516  tgjustf  28563  tgjustr  28564  wlksnwwlknvbij  29998  clwwlkvbij  30205  aciunf1lem  32758  locfinref  34037  tz9.1regs  35330  fnimage  36170  fnessref  36600  refssfne  36601  filnetlem4  36624  dfttc3gw  36766  bj-restb  37467  fin2so  37989  unirep  38096  indexa  38115  nssd  45566  choicefi  45660  axccdom  45681  stoweidlem5  46462  stoweidlem27  46484  stoweidlem28  46485  stoweidlem31  46488  stoweidlem43  46500  stoweidlem44  46501  stoweidlem51  46508  stoweidlem59  46516  nsssmfmbflem  47235  fundcmpsurinjpreimafv  47897  sprbisymrel  47988  uspgrbisymrelALT  48660