Theorem spcegv 3552

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-clel 2803

This theorem is referenced by:  spcedv  3553  spcev  3561  eqeu  3666  absneu  4680  issn  4783  elpreqprlem  4817  elunii  4863  axpweq  5290  brcogw  5811  opeldmd  5849  breldmg  5852  dmsnopg  6162  predtrss  6270  fvrnressn  7095  f1oexbi  7861  unielxp  7962  frrlem13  8231  f1oen4g  8890  f1dom4g  8891  f1oen3g  8892  f1dom3g  8893  f1domg  8897  en2sn  8966  en2prd  8973  fodomr  9045  fodomfir  9218  ordiso  9408  fowdom  9463  inf0  9517  infeq5i  9532  oncard  9856  cardsn  9865  dfac8b  9925  ac10ct  9928  aceq3lem  10014  dfacacn  10036  cflem  10139  cflemOLD  10140  cflecard  10147  cfslb  10160  coftr  10167  alephsing  10170  fin4i  10192  axdc4lem  10349  gchi  10518  hasheqf1oi  14258  relexpindlem  14970  climeu  15462  brcici  17707  initoeu2lem2  17922  gsumval2a  18559  irinitoringc  21386  uptx  23510  alexsubALTlem1  23932  ptcmplem3  23939  prdsxmslem2  24415  tgjustf  28418  tgjustr  28419  wlksnwwlknvbij  29853  clwwlkvbij  30057  aciunf1lem  32606  locfinref  33814  tz9.1regs  35073  fnimage  35913  fnessref  36341  refssfne  36342  filnetlem4  36365  bj-restb  37078  fin2so  37597  unirep  37704  indexa  37723  nssd  45093  choicefi  45188  axccdom  45210  stoweidlem5  45996  stoweidlem27  46018  stoweidlem28  46019  stoweidlem31  46022  stoweidlem43  46034  stoweidlem44  46035  stoweidlem51  46042  stoweidlem59  46050  nsssmfmbflem  46769  fundcmpsurinjpreimafv  47402  sprbisymrel  47493  uspgrbisymrelALT  48149