MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  spcegv Structured version   Visualization version   GIF version

Theorem spcegv 3596
Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2140, ax-11 2156. (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
StepHypRef Expression
1 elisset 2822 . 2 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
2 spcgv.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
32biimprcd 250 . . 3 (𝜓 → (𝑥 = 𝐴𝜑))
43eximdv 1916 . 2 (𝜓 → (∃𝑥 𝑥 = 𝐴 → ∃𝑥𝜑))
51, 4syl5com 31 1 (𝐴𝑉 → (𝜓 → ∃𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1539  wex 1778  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-clel 2815
This theorem is referenced by:  spcedv  3597  spcev  3605  eqeu  3711  absneu  4727  issn  4831  elpreqprlem  4865  elunii  4911  axpweq  5350  brcogw  5878  opeldmd  5916  breldmg  5919  dmsnopg  6232  predtrss  6342  fvrnressn  7180  f1oexbi  7951  unielxp  8053  frrlem13  8324  f1oen4g  9006  f1dom4g  9007  f1oen3g  9008  f1dom3g  9009  f1domg  9013  en2sn  9082  en2prd  9089  fodomr  9169  fodomfir  9369  ordiso  9557  fowdom  9612  inf0  9662  infeq5i  9677  oncard  10001  cardsn  10010  dfac8b  10072  ac10ct  10075  aceq3lem  10161  dfacacn  10183  cflem  10286  cflemOLD  10287  cflecard  10294  cfslb  10307  coftr  10314  alephsing  10317  fin4i  10339  axdc4lem  10496  gchi  10665  hasheqf1oi  14391  relexpindlem  15103  climeu  15592  brcici  17845  initoeu2lem2  18061  gsumval2a  18699  irinitoringc  21491  uptx  23634  alexsubALTlem1  24056  ptcmplem3  24063  prdsxmslem2  24543  tgjustf  28482  tgjustr  28483  wlksnwwlknvbij  29929  clwwlkvbij  30133  aciunf1lem  32673  locfinref  33841  fnimage  35931  fnessref  36359  refssfne  36360  filnetlem4  36383  bj-restb  37096  fin2so  37615  unirep  37722  indexa  37741  nssd  45115  choicefi  45210  axccdom  45232  stoweidlem5  46025  stoweidlem27  46047  stoweidlem28  46048  stoweidlem31  46051  stoweidlem43  46063  stoweidlem44  46064  stoweidlem51  46071  stoweidlem59  46079  nsssmfmbflem  46798  fundcmpsurinjpreimafv  47400  sprbisymrel  47491  uspgrbisymrelALT  48076
  Copyright terms: Public domain W3C validator