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

Theorem rspcdva 3611
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 3604 . 2 (𝐶𝐴 → (∀𝑥𝐴 𝜓𝜒))
51, 2, 4sylc 65 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wcel 2115  wral 3133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-clel 2896  df-ral 3138
This theorem is referenced by:  nvocnv  7027  knatar  7099  caofref  7425  caofinvl  7426  tfisi  7563  suppssov1  7852  wfrlem17  7961  tfrlem1  8002  tfrlem5  8006  marypha1lem  8888  marypha1  8889  ordtypelem6  8978  ordtypelem7  8979  wemaplem2  9002  oemapvali  9138  cantnflem1c  9141  infxpenlem  9431  acni  9463  dfac9  9554  dfac12lem2  9562  sornom  9691  fin1ai  9707  fin2i  9709  fin23lem11  9731  isfin2-2  9733  fin23lem17  9752  fin23lem39  9764  fin1a2lem13  9826  hsmexlem4  9843  ttukeylem5  9927  ttukeylem6  9928  canth4  10061  pwfseqlem5  10077  winalim2  10110  wununi  10120  wunpw  10121  dedekind  10795  zsupss  12330  uzwo3  12336  seqcl2  13389  seqcl  13391  seqf  13392  seqfveq2  13393  seqfveq  13395  seqshft2  13397  monoord  13401  monoord2  13402  sermono  13403  seqsplit  13404  seqcaopr3  13406  seqid  13416  seqid2  13417  seqhomo  13418  seqz  13419  discr1  13601  discr  13602  hashbclem  13811  wrdind  14080  limsupgre  14834  climi  14863  rlimi  14866  rlimclim1  14898  rlimclim  14899  climrlim2  14900  rlimcn1  14941  climcn1  14944  isercoll2  15021  caucvgrlem  15025  caucvgb  15032  iseraltlem2  15035  iseraltlem3  15036  fsumm1  15102  fsum1p  15104  fsumcom2  15125  fsumge1  15148  telfsumo  15153  telfsumo2  15154  fsumparts  15157  o1fsum  15164  isum1p  15192  isumnn0nn  15193  isumrpcl  15194  climcndslem1  15200  climcndslem2  15201  climcnds  15202  cvgrat  15235  mertenslem1  15236  mertens  15238  fprodm1  15317  fprod1p  15318  fprodcom2  15334  prmind2  16023  pcmpt2  16223  prmpwdvds  16234  prmreclem4  16249  prmreclem5  16250  vdwlem1  16311  vdwlem2  16312  vdwlem9  16319  vdwlem10  16320  rami  16345  ramcl  16359  prmodvdslcmf  16377  prmgaplcmlem1  16381  cshwsidrepsw  16423  prdsbasprj  16741  isacs2  16920  acsfiel  16921  catidex  16941  iscatd2  16948  catlid  16950  catrid  16951  subcidcl  17110  funcid  17136  yonedalem4c  17523  yonffthlem  17528  isdrs2  17545  luble  17593  glble  17606  joinle  17620  meetle  17634  poslubmo  17752  posglbmo  17753  acsdrsel  17773  isacs4lem  17774  isacs5lem  17775  acsdrscl  17776  acsficl  17777  lidrideqd  17875  grprinvlem  17879  grprinvd  17880  mndind  17988  grpidd2  18137  mulgsubcl  18238  issubg4  18294  ghmf1  18383  fislw  18746  efgsdmi  18854  efgsrel  18856  gexexlem  18968  gsumzaddlem  19037  gsummhm2  19055  dprdcntz  19126  dprddisj  19127  dprdss  19147  dprd2dlem2  19158  dprd2da  19160  dpjrid  19180  ablfac1eu  19191  pgpfac1lem1  19192  pgpfaclem2  19200  issrngd  19625  islbs2  19919  lbsextlem4  19926  mplsubglem  20207  mpllsslem  20208  subrgasclcl  20272  mplind  20275  evlslem1  20288  prmirredlem  20633  psgndiflemB  20737  frlmphl  20918  mdetralt  21210  mdetunilem1  21214  lmcvg  21863  iscncl  21870  lmff  21902  cnrmi  21961  cmpcov  21990  fiuncmp  22005  hauscmplem  22007  1stcfb  22046  1stcelcls  22062  restnlly  22083  islly2  22085  lly1stc  22097  kgeni  22138  ptpjpre1  22172  ptbasfi  22182  ptpjopn  22213  dfac14  22219  txtube  22241  cnmpt11  22264  cnmpt21  22272  cnmptkp  22281  cnmptk1p  22286  qtopomap  22319  qtopcmap  22320  flimcf  22583  fclscf  22626  flfcntr  22644  ptcmplem3  22655  tgpt0  22720  tsmsi  22735  tsmsxplem2  22755  tsmsxp  22756  isucn2  22881  ucnima  22883  ucncn  22887  cfiluweak  22897  cuspcvg  22903  imasdsf1olem  22976  lpbl  23106  comet  23116  cfilucfil  23162  cnheiborlem  23555  cnheibor  23556  bndth  23559  nmoleub2lem2  23717  nmoleub3  23720  ipcau2  23834  tcphcphlem1  23835  tcphcphlem2  23836  lmmcvg  23861  cmetcaulem  23888  iscmet3lem1  23891  iscmet3lem2  23892  pjthlem1  24037  pjthlem2  24038  ivthlem1  24051  ivthlem2  24052  ivthlem3  24053  ivth2  24055  ivthle  24056  ivthle2  24057  ivthicc  24058  ovoliunlem1  24102  ovolshftlem1  24109  ovolscalem1  24113  ovolicc2lem3  24119  ovolicc2lem4  24120  ovolicc2  24122  volsup  24156  dyadmbl  24200  vitalilem2  24209  vitalilem3  24210  mbfdm  24226  ismbf3d  24254  cncombf  24258  itg2seq  24342  itg2monolem2  24351  itg2monolem3  24352  itg2mono  24353  iblitg  24368  itgconst  24418  itgfsum  24426  limcvallem  24470  cnlimci  24488  cnmptlimc  24489  dvferm1lem  24583  dvferm1  24584  dvferm2lem  24585  dvferm2  24586  dvlipcn  24593  dvle  24606  lhop1lem  24612  dvfsumge  24621  dvfsumlem2  24626  dvfsumlem3  24627  ftc1a  24636  ftc1lem4  24638  itgsubstlem  24647  mdeglt  24662  deg1lt  24694  ply1divex  24733  fta1glem2  24763  fta1g  24764  plyco0  24785  plyeq0lem  24803  dgrcolem2  24867  plydivlem4  24888  plydivex  24889  fta1lem  24899  vieta1lem2  24903  vieta1  24904  tayl0  24953  ulmi  24977  ulmdvlem1  24991  ulmdvlem3  24993  ulmdv  24994  mtest  24995  pserulm  25013  efif1olem4  25133  rlimcnp  25547  rlimcnp2  25548  xrlimcnp  25550  scvxcvx  25567  lgamgulmlem5  25614  lgambdd  25618  lgamcvglem  25621  wilthlem2  25650  fsumdvdscom  25766  musumsum  25773  chtub  25792  fsumvma  25793  perfectlem2  25810  dchrelbas3  25818  dchrelbasd  25819  dchrn0  25830  dchrptlem2  25845  lgsval2lem  25887  lgsdirnn0  25924  lgsdinn0  25925  2sqlem10  26008  dchrisumlem1  26069  dchrmusum2  26074  dchrvmasumlem2  26078  dchrvmasumlem3  26079  dchrvmasumiflem1  26081  dchrisum0flblem2  26089  dchrisum0flb  26090  dchrisum0lem1b  26095  dchrisum0lem2  26098  2vmadivsumlem  26120  chpdifbndlem1  26133  selberg3lem1  26137  selberg4lem1  26140  pntrsumbnd2  26147  pntrlog2bndlem2  26158  pntrlog2bndlem3  26159  pntrlog2bndlem5  26161  pntrlog2bndlem6  26163  pntibndlem2  26171  pntibndlem3  26172  pntlemn  26180  pntlemj  26183  pntlemi  26184  pntlemo  26187  pntleme  26188  pntlem3  26189  pntlemp  26190  ostth2lem1  26198  ostthlem1  26207  ostth2lem2  26214  ostth3  26218  tglowdim1i  26291  tglowdim2ln  26441  wlkonl1iedg  27451  wlkp1lem7  27465  wlkp1lem8  27466  crctcshwlkn0lem6  27597  eupth2eucrct  27998  eupth2lem3  28017  ubthlem1  28649  ubthlem2  28650  minvecolem3  28655  occllem  29082  pjhthlem1  29170  wrdt2ind  30631  mgccole1  30676  mcgmnt2  30679  dfmgc2  30682  0nellinds  30960  linds2eq  30967  prmidl  30984  mxidlmax  31002  ssmxidl  31007  lbsdiflsp0  31050  fedgmullem1  31053  fedgmullem2  31054  extdg1id  31081  ofcfeqd2  31385  inelpisys  31438  unelldsys  31442  ldgenpisyslem1  31447  mbfmcnvima  31540  signstfvneq0  31867  fsum2dsub  31903  hgt750lemc  31943  hgt750lemd  31944  hgt749d  31945  hgt750lemf  31949  bnj1379  32127  bnj1450  32347  revwlk  32396  cvmlift2lem10  32584  fpr3g  33147  unblimceq0lem  33870  unblimceq0  33871  unbdqndv2  33875  bj-ismoored  34435  lcmineqlem4  39226  fnwe2lem2  39848  aomclem4  39854  scottelrankd  40812  mnuop123d  40827  mnuprdlem1  40837  mnuprdlem2  40838  eliind  41562  rnmptbd2lem  41748  rnmptbdlem  41755  limclner  42156  climisp  42251  climrescn  42253  climxrrelem  42254  climxrre  42255  cncfshift  42379  cncfperiod  42384  fperdvper  42424  salunicl  42821  saldifcl  42824  meadjuni  42959
  Copyright terms: Public domain W3C validator