Theorem spcegv 3555

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ∃wex 1808   ∈ wcel 2142

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-clel 2837

This theorem is used by:  spcedv  3556  spcev  3564  eqeu  3668  absneu  4693  issn  4796  elpreqprlem  4830  elunii  4876  axpweq  5320  brcogw  5853  opeldmd  5895  breldmg  5898  dmsnopg  6213  predtrss  6323  fvrnressn  7158  f1oexbi  7923  unielxp  8022  frrlem13  8293  f1oen4g  8959  f1dom4g  8960  f1oen3g  8961  f1dom3g  8962  f1domg  8966  en2sn  9036  en2prd  9042  fodomr  9114  fodomfir  9285  ordiso  9476  fowdom  9531  inf0  9588  infeq5i  9603  oncard  9953  cardsn  9962  dfac8b  10022  ac10ct  10025  aceq3lem  10111  dfacacn  10132  cflem  10235  cflecard  10242  cfslb  10256  coftr  10263  alephsing  10266  fin4i  10288  axdc4lem  10445  gchi  10615  hasheqf1oi  14394  relexpindlem  15107  climeu  15613  brcici  17863  initoeu2lem2  18078  gsumval2a  18749  irinitoringc  21640  uptx  23793  alexsubALTlem1  24215  ptcmplem3  24222  prdsxmslem2  24697  tgjustf  28753  tgjustr  28754  wlksnwwlknvbij  30268  clwwlkvbij  30475  aciunf1lem  33018  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