Theorem spcegv 3552

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2178, ax-11 2194. (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 2843	. 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 2145

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 2147

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

This theorem is used by:  spcedv  3553  spcev  3561  eqeu  3664  absneu  4689  issn  4792  elpreqprlem  4826  elunii  4872  axpweq  5312  brcogw  5846  opeldmd  5888  breldmg  5891  dmsnopg  6214  predtrss  6325  fvrnressn  7165  f1oexbi  7940  unielxp  8039  frrlem13  8316  f1oen4g  8991  f1dom4g  8992  f1oen3g  8993  f1dom3g  8994  f1domg  8998  en2sn  9069  en2prd  9075  fodomr  9147  fodomfir  9319  ordiso  9510  fowdom  9565  inf0  9622  infeq5i  9637  oncard  10041  cardsn  10050  dfac8b  10110  ac10ct  10113  aceq3lem  10199  dfacacn  10220  cflem  10323  cflecard  10330  cfslb  10344  coftr  10351  alephsing  10354  fin4i  10376  axdc4lem  10533  gchi  10709  hasheqf1oi  14495  relexpindlem  15216  climeu  15722  brcici  17975  initoeu2lem2  18190  gsumval2a  18874  irinitoringc  21785  uptx  23944  alexsubALTlem1  24366  ptcmplem3  24373  prdsxmslem2  24848  tgjustf  28935  tgjustr  28936  wlksnwwlknvbij  30497  clwwlkvbij  30704  aciunf1lem  33256  locfinref  34473  tz9.1regs  35802  fnimage  36691  fnessref  37145  refssfne  37146  filnetlem4  37169  dfttc3gw  37311  bj-restb  38015  fin2so  38530  unirep  38648  indexa  38667  nssd  46119  choicefi  46213  axccdom  46234  stoweidlem5  47014  stoweidlem27  47036  stoweidlem28  47037  stoweidlem31  47040  stoweidlem43  47052  stoweidlem44  47053  stoweidlem51  47060  stoweidlem59  47068  nsssmfmbflem  47787  fundcmpsurinjpreimafv  48489  sprbisymrel  48580  uspgrbisymrelALT  49252