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

Theorem rspcdva 3466
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 3456 . 2 (𝐶𝐴 → (∀𝑥𝐴 𝜓𝜒))
51, 2, 4sylc 65 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631  wcel 2145  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-v 3353
This theorem is referenced by:  nvocnv  6680  knatar  6750  grprinvlem  7019  grprinvd  7020  caofref  7070  caofinvl  7071  tfisi  7205  suppssov1  7479  wfrlem17  7584  tfrlem1  7625  tfrlem5  7629  marypha1lem  8495  marypha1  8496  ordtypelem6  8584  ordtypelem7  8585  wemaplem2  8608  oemapvali  8745  cantnflem1c  8748  infxpenlem  9036  acni  9068  dfac9  9160  dfac12lem2  9168  sornom  9301  fin1ai  9317  fin2i  9319  fin23lem11  9341  isfin2-2  9343  fin23lem17  9362  fin23lem39  9374  fin1a2lem13  9436  hsmexlem4  9453  ttukeylem5  9537  ttukeylem6  9538  canth4  9671  pwfseqlem5  9687  winalim2  9720  wununi  9730  wunpw  9731  dedekind  10402  zsupss  11980  uzwo3  11986  seqcl2  13026  seqcl  13028  seqf  13029  seqfveq2  13030  seqfveq  13032  seqshft2  13034  monoord  13038  monoord2  13039  sermono  13040  seqsplit  13041  seqcaopr3  13043  seqid  13053  seqid2  13054  seqhomo  13055  seqz  13056  discr1  13207  discr  13208  hashbclem  13438  wrdind  13685  limsupgre  14420  climi  14449  rlimi  14452  rlimclim1  14484  rlimclim  14485  climrlim2  14486  rlimcn1  14527  climcn1  14530  isercoll2  14607  caucvgrlem  14611  caucvgb  14618  iseraltlem2  14621  iseraltlem3  14622  fsumm1  14688  fsum1p  14690  fsumcom2  14713  fsumge1  14736  telfsumo  14741  telfsumo2  14742  fsumparts  14745  o1fsum  14752  isum1p  14780  isumnn0nn  14781  isumrpcl  14782  climcndslem1  14788  climcndslem2  14789  climcnds  14790  cvgrat  14822  mertenslem1  14823  mertens  14825  fprodm1  14904  fprod1p  14905  fprodcom2  14921  prmind2  15605  pcmpt2  15804  prmpwdvds  15815  prmreclem4  15830  prmreclem5  15831  vdwlem1  15892  vdwlem2  15893  vdwlem9  15900  vdwlem10  15901  rami  15926  ramcl  15940  prmodvdslcmf  15958  prmgaplcmlem1  15962  cshwsidrepsw  16007  prdsbasprj  16340  isacs2  16521  acsfiel  16522  catidex  16542  iscatd2  16549  catlid  16551  catrid  16552  subcidcl  16711  funcid  16737  yonedalem4c  17125  yonffthlem  17130  isdrs2  17147  luble  17195  glble  17208  joinle  17222  meetle  17236  poslubmo  17354  posglbmo  17355  acsdrsel  17375  isacs4lem  17376  isacs5lem  17377  acsdrscl  17378  acsficl  17379  mrcmndind  17574  grpidd2  17667  mulgsubcl  17763  issubg4  17821  ghmf1  17897  fislw  18247  efgsdmi  18352  efgsrel  18354  gexexlem  18462  gsumzaddlem  18528  gsummhm2  18546  dprdcntz  18615  dprddisj  18616  dprdss  18636  dprd2dlem2  18647  dprd2da  18649  dpjrid  18669  ablfac1eu  18680  pgpfac1lem1  18681  pgpfaclem2  18689  issrngd  19071  islbs2  19369  lbsextlem4  19376  mplsubglem  19649  mpllsslem  19650  subrgasclcl  19714  mplind  19717  evlslem1  19730  prmirredlem  20056  psgndiflemB  20162  frlmphl  20337  mdetralt  20632  mdetunilem1  20636  lmcvg  21287  iscncl  21294  lmff  21326  cnrmi  21385  cmpcov  21413  fiuncmp  21428  hauscmplem  21430  1stcfb  21469  1stcelcls  21485  restnlly  21506  islly2  21508  lly1stc  21520  kgeni  21561  ptpjpre1  21595  ptbasfi  21605  ptpjopn  21636  dfac14  21642  txtube  21664  cnmpt11  21687  cnmpt21  21695  cnmptkp  21704  cnmptk1p  21709  qtopomap  21742  qtopcmap  21743  flimcf  22006  fclscf  22049  flfcntr  22067  ptcmplem3  22078  tgpt0  22142  tsmsi  22157  tsmsxplem2  22177  tsmsxp  22178  isucn2  22303  ucnima  22305  ucncn  22309  cfiluweak  22319  cuspcvg  22325  imasdsf1olem  22398  lpbl  22528  comet  22538  cfilucfil  22584  cnheiborlem  22973  cnheibor  22974  bndth  22977  nmoleub2lem2  23135  nmoleub3  23138  ipcau2  23252  tchcphlem1  23253  tchcphlem2  23254  lmmcvg  23278  cmetcaulem  23305  iscmet3lem1  23308  iscmet3lem2  23309  pjthlem1  23427  pjthlem2  23428  ivthlem1  23439  ivthlem2  23440  ivthlem3  23441  ivth2  23443  ivthle  23444  ivthle2  23445  ivthicc  23446  ovoliunlem1  23490  ovolshftlem1  23497  ovolscalem1  23501  ovolicc2lem3  23507  ovolicc2lem4  23508  ovolicc2  23510  volsup  23544  dyadmbl  23588  vitalilem2  23597  vitalilem3  23598  mbfdm  23614  ismbf3d  23641  cncombf  23645  itg2seq  23729  itg2monolem2  23738  itg2monolem3  23739  itg2mono  23740  iblitg  23755  itgconst  23805  itgfsum  23813  limcvallem  23855  cnlimci  23873  cnmptlimc  23874  dvferm1lem  23967  dvferm1  23968  dvferm2lem  23969  dvferm2  23970  dvlipcn  23977  dvle  23990  lhop1lem  23996  dvfsumge  24005  dvfsumlem2  24010  dvfsumlem3  24011  ftc1a  24020  ftc1lem4  24022  itgsubstlem  24031  mdeglt  24045  deg1lt  24077  ply1divex  24116  fta1glem2  24146  fta1g  24147  plyco0  24168  plyeq0lem  24186  dgrcolem2  24250  plydivlem4  24271  plydivex  24272  fta1lem  24282  vieta1lem2  24286  vieta1  24287  tayl0  24336  ulmi  24360  ulmdvlem1  24374  ulmdvlem3  24376  ulmdv  24377  mtest  24378  pserulm  24396  efif1olem4  24512  rlimcnp  24913  rlimcnp2  24914  xrlimcnp  24916  scvxcvx  24933  lgamgulmlem5  24980  lgambdd  24984  lgamcvglem  24987  wilthlem2  25016  fsumdvdscom  25132  musumsum  25139  chtub  25158  fsumvma  25159  perfectlem2  25176  dchrelbas3  25184  dchrelbasd  25185  dchrn0  25196  dchrptlem2  25211  lgsval2lem  25253  lgsdirnn0  25290  lgsdinn0  25291  2sqlem10  25374  dchrisumlem1  25399  dchrmusum2  25404  dchrvmasumlem2  25408  dchrvmasumlem3  25409  dchrvmasumiflem1  25411  dchrisum0flblem2  25419  dchrisum0flb  25420  dchrisum0lem1b  25425  dchrisum0lem2  25428  2vmadivsumlem  25450  chpdifbndlem1  25463  selberg3lem1  25467  selberg4lem1  25470  pntrsumbnd2  25477  pntrlog2bndlem2  25488  pntrlog2bndlem3  25489  pntrlog2bndlem5  25491  pntrlog2bndlem6  25493  pntibndlem2  25501  pntibndlem3  25502  pntlemn  25510  pntlemj  25513  pntlemi  25514  pntlemo  25517  pntleme  25518  pntlem3  25519  pntlemp  25520  ostth2lem1  25528  ostthlem1  25537  ostth2lem2  25544  ostth3  25548  tglowdim1i  25617  tglowdim2ln  25767  wlkonl1iedg  26796  wlkp1lem7  26811  wlkp1lem8  26812  crctcshwlkn0lem6  26943  eupth2eucrct  27397  eupth2lem3  27416  ubthlem1  28066  ubthlem2  28067  minvecolem3  28072  occllem  28502  pjhthlem1  28590  inelpisys  30557  unelldsys  30561  ldgenpisyslem1  30566  fsum2dsub  31025  hgt750lemc  31065  hgt750lemd  31066  hgt749d  31067  hgt750lemf  31071  cvmlift2lem10  31632  unblimceq0lem  32834  unblimceq0  32835  unbdqndv2  32839  climisp  40496  climrescn  40498  climxrrelem  40499  climxrre  40500  saldifcl  41056
  Copyright terms: Public domain W3C validator