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

Theorem rspcdva 3507
Description: Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.)
Hypotheses
Ref Expression
rspcdva.1 (𝑥 = 𝐶 → (𝜓𝜒))
rspcdva.2 (𝜑 → ∀𝑥𝐴 𝜓)
rspcdva.3 (𝜑𝐶𝐴)
Assertion
Ref Expression
rspcdva (𝜑𝜒)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜒,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rspcdva
StepHypRef Expression
1 rspcdva.3 . 2 (𝜑𝐶𝐴)
2 rspcdva.2 . 2 (𝜑 → ∀𝑥𝐴 𝜓)
3 rspcdva.1 . . 3 (𝑥 = 𝐶 → (𝜓𝜒))
43rspcv 3497 . 2 (𝐶𝐴 → (∀𝑥𝐴 𝜓𝜒))
51, 2, 4sylc 65 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  wcel 2158  wral 3095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ral 3100  df-v 3392
This theorem is referenced by:  nvocnv  6758  knatar  6828  grprinvlem  7099  grprinvd  7100  caofref  7150  caofinvl  7151  tfisi  7285  suppssov1  7559  wfrlem17  7664  tfrlem1  7705  tfrlem5  7709  marypha1lem  8575  marypha1  8576  ordtypelem6  8664  ordtypelem7  8665  wemaplem2  8688  oemapvali  8825  cantnflem1c  8828  infxpenlem  9116  acni  9148  dfac9  9240  dfac12lem2  9248  sornom  9381  fin1ai  9397  fin2i  9399  fin23lem11  9421  isfin2-2  9423  fin23lem17  9442  fin23lem39  9454  fin1a2lem13  9516  hsmexlem4  9533  ttukeylem5  9617  ttukeylem6  9618  canth4  9751  pwfseqlem5  9767  winalim2  9800  wununi  9810  wunpw  9811  dedekind  10482  zsupss  11992  uzwo3  11998  seqcl2  13038  seqcl  13040  seqf  13041  seqfveq2  13042  seqfveq  13044  seqshft2  13046  monoord  13050  monoord2  13051  sermono  13052  seqsplit  13053  seqcaopr3  13055  seqid  13065  seqid2  13066  seqhomo  13067  seqz  13068  discr1  13219  discr  13220  hashbclem  13449  wrdind  13696  limsupgre  14431  climi  14460  rlimi  14463  rlimclim1  14495  rlimclim  14496  climrlim2  14497  rlimcn1  14538  climcn1  14541  isercoll2  14618  caucvgrlem  14622  caucvgb  14629  iseraltlem2  14632  iseraltlem3  14633  fsumm1  14699  fsum1p  14701  fsumcom2  14724  fsumge1  14747  telfsumo  14752  telfsumo2  14753  fsumparts  14756  o1fsum  14763  isum1p  14791  isumnn0nn  14792  isumrpcl  14793  climcndslem1  14799  climcndslem2  14800  climcnds  14801  cvgrat  14832  mertenslem1  14833  mertens  14835  fprodm1  14914  fprod1p  14915  fprodcom2  14931  prmind2  15612  pcmpt2  15810  prmpwdvds  15821  prmreclem4  15836  prmreclem5  15837  vdwlem1  15898  vdwlem2  15899  vdwlem9  15906  vdwlem10  15907  rami  15932  ramcl  15946  prmodvdslcmf  15964  prmgaplcmlem1  15968  cshwsidrepsw  16008  prdsbasprj  16333  isacs2  16514  acsfiel  16515  catidex  16535  iscatd2  16542  catlid  16544  catrid  16545  subcidcl  16704  funcid  16730  yonedalem4c  17118  yonffthlem  17123  isdrs2  17140  luble  17188  glble  17201  joinle  17215  meetle  17229  poslubmo  17347  posglbmo  17348  acsdrsel  17368  isacs4lem  17369  isacs5lem  17370  acsdrscl  17371  acsficl  17372  mrcmndind  17567  grpidd2  17660  mulgsubcl  17756  issubg4  17811  ghmf1  17887  fislw  18237  efgsdmi  18342  efgsrel  18344  gexexlem  18452  gsumzaddlem  18518  gsummhm2  18536  dprdcntz  18605  dprddisj  18606  dprdss  18626  dprd2dlem2  18637  dprd2da  18639  dpjrid  18659  ablfac1eu  18670  pgpfac1lem1  18671  pgpfaclem2  18679  issrngd  19061  islbs2  19359  lbsextlem4  19366  mplsubglem  19639  mpllsslem  19640  subrgasclcl  19703  mplind  19706  evlslem1  19719  prmirredlem  20045  psgndiflemB  20150  frlmphl  20326  mdetralt  20621  mdetunilem1  20625  lmcvg  21276  iscncl  21283  lmff  21315  cnrmi  21374  cmpcov  21402  fiuncmp  21417  hauscmplem  21419  1stcfb  21458  1stcelcls  21474  restnlly  21495  islly2  21497  lly1stc  21509  kgeni  21550  ptpjpre1  21584  ptbasfi  21594  ptpjopn  21625  dfac14  21631  txtube  21653  cnmpt11  21676  cnmpt21  21684  cnmptkp  21693  cnmptk1p  21698  qtopomap  21731  qtopcmap  21732  flimcf  21995  fclscf  22038  flfcntr  22056  ptcmplem3  22067  tgpt0  22131  tsmsi  22146  tsmsxplem2  22166  tsmsxp  22167  isucn2  22292  ucnima  22294  ucncn  22298  cfiluweak  22308  cuspcvg  22314  imasdsf1olem  22387  lpbl  22517  comet  22527  cfilucfil  22573  cnheiborlem  22962  cnheibor  22963  bndth  22966  nmoleub2lem2  23124  nmoleub3  23127  ipcau2  23241  tchcphlem1  23242  tchcphlem2  23243  lmmcvg  23267  cmetcaulem  23294  iscmet3lem1  23297  iscmet3lem2  23298  pjthlem1  23416  pjthlem2  23417  ivthlem1  23428  ivthlem2  23429  ivthlem3  23430  ivth2  23432  ivthle  23433  ivthle2  23434  ivthicc  23435  ovoliunlem1  23479  ovolshftlem1  23486  ovolscalem1  23490  ovolicc2lem3  23496  ovolicc2lem4  23497  ovolicc2  23499  volsup  23533  dyadmbl  23577  vitalilem2  23586  vitalilem3  23587  mbfdm  23603  ismbf3d  23631  cncombf  23635  itg2seq  23719  itg2monolem2  23728  itg2monolem3  23729  itg2mono  23730  iblitg  23745  itgconst  23795  itgfsum  23803  limcvallem  23845  cnlimci  23863  cnmptlimc  23864  dvferm1lem  23957  dvferm1  23958  dvferm2lem  23959  dvferm2  23960  dvlipcn  23967  dvle  23980  lhop1lem  23986  dvfsumge  23995  dvfsumlem2  24000  dvfsumlem3  24001  ftc1a  24010  ftc1lem4  24012  itgsubstlem  24021  mdeglt  24035  deg1lt  24067  ply1divex  24106  fta1glem2  24136  fta1g  24137  plyco0  24158  plyeq0lem  24176  dgrcolem2  24240  plydivlem4  24261  plydivex  24262  fta1lem  24272  vieta1lem2  24276  vieta1  24277  tayl0  24326  ulmi  24350  ulmdvlem1  24364  ulmdvlem3  24366  ulmdv  24367  mtest  24368  pserulm  24386  efif1olem4  24502  rlimcnp  24902  rlimcnp2  24903  xrlimcnp  24905  scvxcvx  24922  lgamgulmlem5  24969  lgambdd  24973  lgamcvglem  24976  wilthlem2  25005  fsumdvdscom  25121  musumsum  25128  chtub  25147  fsumvma  25148  perfectlem2  25165  dchrelbas3  25173  dchrelbasd  25174  dchrn0  25185  dchrptlem2  25200  lgsval2lem  25242  lgsdirnn0  25279  lgsdinn0  25280  2sqlem10  25363  dchrisumlem1  25388  dchrmusum2  25393  dchrvmasumlem2  25397  dchrvmasumlem3  25398  dchrvmasumiflem1  25400  dchrisum0flblem2  25408  dchrisum0flb  25409  dchrisum0lem1b  25414  dchrisum0lem2  25417  2vmadivsumlem  25439  chpdifbndlem1  25452  selberg3lem1  25456  selberg4lem1  25459  pntrsumbnd2  25466  pntrlog2bndlem2  25477  pntrlog2bndlem3  25478  pntrlog2bndlem5  25480  pntrlog2bndlem6  25482  pntibndlem2  25490  pntibndlem3  25491  pntlemn  25499  pntlemj  25502  pntlemi  25503  pntlemo  25506  pntleme  25507  pntlem3  25508  pntlemp  25509  ostth2lem1  25517  ostthlem1  25526  ostth2lem2  25533  ostth3  25537  tglowdim1i  25606  tglowdim2ln  25756  wlkonl1iedg  26785  wlkp1lem7  26800  wlkp1lem8  26801  crctcshwlkn0lem6  26932  eupth2eucrct  27386  eupth2lem3  27405  ubthlem1  28051  ubthlem2  28052  minvecolem3  28057  occllem  28487  pjhthlem1  28575  inelpisys  30539  unelldsys  30543  ldgenpisyslem1  30548  fsum2dsub  31007  hgt750lemc  31047  hgt750lemd  31048  hgt749d  31049  hgt750lemf  31053  cvmlift2lem10  31614  unblimceq0lem  32811  unblimceq0  32812  unbdqndv2  32816  limclner  40360  climisp  40455  climrescn  40457  climxrrelem  40458  climxrre  40459  cncfshift  40564  cncfperiod  40569  fperdvper  40610  saldifcl  41015
  Copyright terms: Public domain W3C validator