Theorem spcegv 3558

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-clel 2840

This theorem is used by:  spcedv  3559  spcev  3567  eqeu  3671  absneu  4696  issn  4799  elpreqprlem  4833  elunii  4879  axpweq  5323  brcogw  5856  opeldmd  5898  breldmg  5901  dmsnopg  6216  predtrss  6327  fvrnressn  7164  f1oexbi  7931  unielxp  8030  frrlem13  8301  f1oen4g  8967  f1dom4g  8968  f1oen3g  8969  f1dom3g  8970  f1domg  8974  en2sn  9045  en2prd  9051  fodomr  9123  fodomfir  9294  ordiso  9485  fowdom  9540  inf0  9597  infeq5i  9612  oncard  9962  cardsn  9971  dfac8b  10031  ac10ct  10034  aceq3lem  10120  dfacacn  10141  cflem  10244  cflecard  10251  cfslb  10265  coftr  10272  alephsing  10275  fin4i  10297  axdc4lem  10454  gchi  10628  hasheqf1oi  14409  relexpindlem  15128  climeu  15634  brcici  17883  initoeu2lem2  18098  gsumval2a  18779  irinitoringc  21683  uptx  23837  alexsubALTlem1  24259  ptcmplem3  24266  prdsxmslem2  24741  tgjustf  28797  tgjustr  28798  wlksnwwlknvbij  30328  clwwlkvbij  30535  aciunf1lem  33082  locfinref  34299  tz9.1regs  35608  fnimage  36460  fnessref  36929  refssfne  36930  filnetlem4  36953  dfttc3gw  37095  bj-restb  37797  fin2so  38319  unirep  38427  indexa  38446  nssd  45900  choicefi  45994  axccdom  46015  stoweidlem5  46796  stoweidlem27  46818  stoweidlem28  46819  stoweidlem31  46822  stoweidlem43  46834  stoweidlem44  46835  stoweidlem51  46842  stoweidlem59  46850  nsssmfmbflem  47569  fundcmpsurinjpreimafv  48234  sprbisymrel  48325  uspgrbisymrelALT  48997