Theorem spcegv 3556

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∃wex 1809   ∈ wcel 2143

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-clel 2838

This theorem is used by:  spcedv  3557  spcev  3565  eqeu  3669  absneu  4694  issn  4797  elpreqprlem  4831  elunii  4877  axpweq  5321  brcogw  5854  opeldmd  5896  breldmg  5899  dmsnopg  6214  predtrss  6323  fvrnressn  7158  f1oexbi  7921  unielxp  8020  frrlem13  8291  f1oen4g  8957  f1dom4g  8958  f1oen3g  8959  f1dom3g  8960  f1domg  8964  en2sn  9034  en2prd  9040  fodomr  9112  fodomfir  9283  ordiso  9474  fowdom  9529  inf0  9586  infeq5i  9601  oncard  9951  cardsn  9960  dfac8b  10020  ac10ct  10023  aceq3lem  10109  dfacacn  10130  cflem  10233  cflecard  10240  cfslb  10254  coftr  10261  alephsing  10264  fin4i  10286  axdc4lem  10443  gchi  10613  hasheqf1oi  14392  relexpindlem  15105  climeu  15611  brcici  17861  initoeu2lem2  18076  gsumval2a  18747  irinitoringc  21638  uptx  23791  alexsubALTlem1  24213  ptcmplem3  24220  prdsxmslem2  24695  tgjustf  28751  tgjustr  28752  wlksnwwlknvbij  30266  clwwlkvbij  30473  aciunf1lem  33016  locfinref  34240  tz9.1regs  35555  fnimage  36427  fnessref  36896  refssfne  36897  filnetlem4  36920  dfttc3gw  37062  bj-restb  37764  fin2so  38286  unirep  38393  indexa  38412  nssd  45851  choicefi  45945  axccdom  45966  stoweidlem5  46747  stoweidlem27  46769  stoweidlem28  46770  stoweidlem31  46773  stoweidlem43  46785  stoweidlem44  46786  stoweidlem51  46793  stoweidlem59  46801  nsssmfmbflem  47520  fundcmpsurinjpreimafv  48185  sprbisymrel  48276  uspgrbisymrelALT  48948