Theorem spcegv 3581

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533  ∃wex 1773   ∈ wcel 2098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-clel 2802

This theorem is referenced by:  spcedv  3582  spcev  3590  eqeu  3698  absneu  4734  issn  4835  elpreqprlem  4868  elunii  4914  axpweq  5350  brcogw  5871  opeldmd  5909  breldmg  5912  dmsnopg  6219  predtrss  6330  fvrnressn  7170  f1oexbi  7936  unielxp  8032  frrlem13  8304  f1oen4g  8985  f1dom4g  8986  f1oen3g  8987  f1dom3g  8988  f1domg  8993  en2sn  9067  en2snOLD  9068  en2prd  9076  fodomr  9156  ordiso  9546  fowdom  9601  inf0  9651  infeq5i  9666  oncard  9990  cardsn  9999  dfac8b  10061  ac10ct  10064  aceq3lem  10150  dfacacn  10171  cflem  10276  cflecard  10283  cfslb  10296  coftr  10303  alephsing  10306  fin4i  10328  axdc4lem  10485  gchi  10654  hasheqf1oi  14354  relexpindlem  15054  climeu  15543  brcici  17802  initoeu2lem2  18023  gsumval2a  18664  irinitoringc  21439  uptx  23590  alexsubALTlem1  24012  ptcmplem3  24019  prdsxmslem2  24499  tgjustf  28369  tgjustr  28370  wlksnwwlknvbij  29811  clwwlkvbij  30015  aciunf1lem  32549  locfinref  33593  fnimage  35676  fnessref  35992  refssfne  35993  filnetlem4  36016  bj-restb  36724  fin2so  37231  unirep  37338  indexa  37357  nssd  44616  choicefi  44717  axccdom  44739  stoweidlem5  45536  stoweidlem27  45558  stoweidlem28  45559  stoweidlem31  45562  stoweidlem43  45574  stoweidlem44  45575  stoweidlem51  45582  stoweidlem59  45590  nsssmfmbflem  46309  fundcmpsurinjpreimafv  46890  sprbisymrel  46981  uspgrbisymrelALT  47408