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

Theorem rspcv 3278
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
Hypothesis
Ref Expression
rspcv.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rspcv (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcv
StepHypRef Expression
1 nfv 1830 . 2 𝑥𝜓
2 rspcv.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2rspc 3276 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175
This theorem is referenced by:  rspccv  3279  rspcva  3280  rspccva  3281  rspcda  3287  rspc3v  3296  rr19.3v  3314  rr19.28v  3315  rspsbc  3484  intmin  4432  ralxfrALT  4813  somo  4993  fr2nr  5016  nvocnv  6437  weniso  6504  knatar  6507  grprinvlem  6770  grprinvd  6771  caofref  6821  fr3nr  6871  limuni3  6944  tfinds  6951  funcnvuni  7012  suppfnss  7207  onnseq  7328  smo11  7348  tfrlem1  7359  tfrlem5  7363  tfrlem9  7368  tz7.49  7427  omeulem1  7549  oeordi  7554  nneneq  8028  frfi  8090  unblem2  8098  unbnn2  8102  xpfi  8116  ordiso2  8303  ordtypelem6  8311  ordtypelem7  8312  cantnflem1c  8467  cantnflem1  8469  rankunb  8596  tcrank  8630  carduni  8690  dfac8alem  8735  acni  8751  alephinit  8801  aceq3lem  8826  dfac5  8834  dfac12lem2  8849  dfac12r  8851  dfac12k  8852  pwsdompw  8909  cflm  8955  fin1ai  8998  fin2i  9000  isfin2-2  9024  fin23lem17  9043  fin23lem39  9055  isf32lem1  9058  isf32lem2  9059  isf34lem4  9082  hsmexlem4  9134  axcc3  9143  domtriomlem  9147  axdc3lem2  9156  axdc4lem  9160  axcclem  9162  ttukeylem5  9218  ttukeylem6  9219  axdclem  9224  alephval2  9273  canth4  9348  pwfseqlem5  9364  winainflem  9394  wununi  9407  wunpw  9408  eltskm  9544  dedekind  10079  squeeze0  10805  fiminre  10851  lbreu  10852  nnsub  10936  ublbneg  11649  zsupss  11653  uzwo3  11659  zmax  11661  zbtwnre  11662  xrub  12014  infmremnf  12044  infmrp1  12045  fzrevral  12294  axdc4uzlem  12644  seqcl2  12681  seqcl  12683  seqf  12684  seqfveq2  12685  seqfveq  12687  seqshft2  12689  monoord  12693  monoord2  12694  sermono  12695  seqsplit  12696  seqcaopr3  12698  seqid  12708  seqid2  12709  seqhomo  12710  seqz  12711  discr1  12862  discr  12863  faclbnd4lem4  12945  hashbclem  13093  ccatalpha  13228  wrdind  13328  wrd2ind  13329  reuccats1lem  13331  recan  13924  cau3lem  13942  caubnd2  13945  limsupgre  14060  climi  14089  rlimi  14092  rlimclim1  14124  rlimclim  14125  climrlim2  14126  climshftlem  14153  rlimcld2  14157  rlimcn1  14167  climcn1  14170  subcn2  14173  isercoll  14246  isercoll2  14247  climcau  14249  caucvgrlem  14251  caucvgb  14258  serf0  14259  iseraltlem2  14261  iseraltlem3  14262  iseralt  14263  fsumm1  14324  fsum1p  14326  fsumcom2  14347  fsumcom2OLD  14348  fsumge1  14370  telfsumo  14375  telfsumo2  14376  fsumparts  14379  o1fsum  14386  isum1p  14412  isumnn0nn  14413  isumrpcl  14414  climcndslem1  14420  climcndslem2  14421  climcnds  14422  cvgrat  14454  mertenslem1  14455  mertens  14457  clim2prod  14459  ntrivcvgfvn0  14470  fprodm1  14536  fprod1p  14537  fprodcom2  14553  fprodcom2OLD  14554  sqrt2irr  14817  ndvdssub  14971  dfgcd2  15101  lcmf  15184  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  lcmfdvds  15193  lcmfdvdsb  15194  lcmfunsn  15195  coprmgcdb  15200  coprmdvds1  15203  coprmprod  15213  coprmproddvdslem  15214  prmind2  15236  nprm  15239  dvdsprm  15253  coprm  15261  pcmpt  15434  pcmpt2  15435  pcmptdvds  15436  pcfac  15441  prmpwdvds  15446  unbenlem  15450  prmreclem4  15461  vdwlem1  15523  vdwlem2  15524  vdwlem9  15531  vdwlem10  15532  vdwlem13  15535  vdwnnlem1  15537  rami  15557  ramcl  15571  prmdvdsprmop  15585  prmodvdslcmf  15589  prmgaplcmlem1  15593  prmgaplem7  15599  catidex  16158  catideu  16159  iscatd2  16165  catlid  16167  catrid  16168  subcidcl  16327  funcid  16353  initoid  16478  termoid  16479  initoeu1  16484  termoeu1  16491  yonedalem4c  16740  yonffthlem  16745  isdrs2  16762  lublecllem  16811  lubun  16946  poslubmo  16969  posglbmo  16970  sgrp2rid2ex  17237  dfgrp2  17270  grpidd2  17282  grpidinv2  17297  dfgrp3lem  17336  mulgsubcl  17378  issubg4  17436  ghmf1  17512  fislw  17863  efgi  17955  efgi2  17961  efgsdmi  17968  efgsrel  17970  gexexlem  18078  gsummhm2  18162  dprdcntz  18230  dprddisj  18231  dprdss  18251  dprd2dlem2  18262  dprd2da  18264  dpjrid  18284  pgpfac1lem1  18296  pgpfaclem2  18304  srgrz  18349  srglz  18350  srgisid  18351  f1rhm0to0ALT  18564  issrngd  18684  islmodd  18692  islmhm2  18859  islbs2  18975  lbsextlem4  18982  rrgeq0i  19110  mvrf1  19246  mplsubglem  19255  mpllsslem  19256  subrgasclcl  19320  cply1mul  19485  prmirredlem  19660  ip2eq  19817  frlmphl  19939  mdetralt  20233  isclo2  20702  lmcvg  20876  cnpnei  20878  iscncl  20883  cncls  20888  lmss  20912  lmff  20915  cnt0  20960  isnrm2  20972  cnrmi  20974  isreg2  20991  cmpcov  21002  tgcmp  21014  uncmp  21016  fiuncmp  21017  dfcon2  21032  1stcclb  21057  1stcfb  21058  2ndcctbss  21068  1stcelcls  21074  restnlly  21095  islly2  21097  lly1stc  21109  comppfsc  21145  kgeni  21150  kgencn2  21170  ptpjpre1  21184  ptbasfi  21194  ptpjopn  21225  dfac14  21231  txtube  21253  txlm  21261  cnmpt11  21276  cnmpt21  21284  cnmptkp  21293  cnmptk1p  21298  qtopomap  21331  qtopcmap  21332  kqfvima  21343  kqt0lem  21349  isr0  21350  nrmr0reg  21362  fgss2  21488  isufil2  21522  cfinufil  21542  flimopn  21589  fbflim2  21591  flimcf  21596  flfneii  21606  cnpflf  21615  fclssscls  21632  fclsnei  21633  fclsrest  21638  fclscf  21639  flimfnfcls  21642  fclscmp  21644  isfcf  21648  fcfnei  21649  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  ptcmplem3  21668  tgpt0  21732  tsmsi  21747  tsmsgsum  21752  tsmsres  21757  tsmsxplem1  21766  tsmsxplem2  21767  tsmsxp  21768  ustincl  21821  ustdiag  21822  ustinvel  21823  ustexhalf  21824  ucnima  21895  ucncn  21899  cfiluexsm  21904  psmet0  21923  imasdsf1olem  21988  prdsbl  22106  metss  22123  comet  22128  metcnp3  22155  isngp4  22226  nmoi  22342  mulc1cncf  22516  cncfco  22518  cnheiborlem  22561  cnheibor  22562  bndth  22565  lebnumii  22573  nmoleub2lem2  22724  nmoleub3  22727  ipcau2  22841  tchcphlem1  22842  tchcphlem2  22843  lmmcvg  22867  iscfil3  22879  iscau2  22883  iscau4  22885  cmetcaulem  22894  iscmet3lem1  22897  iscmet3lem2  22898  equivcfil  22905  equivcau  22906  lmcau  22919  pjthlem1  23016  pjthlem2  23017  ivthlem1  23027  ivthlem2  23028  ivthlem3  23029  ivth2  23031  ivthle  23032  ivthle2  23033  ivthicc  23034  ovoliunlem1  23077  ovolshftlem1  23084  ovolscalem1  23088  ovolicc2lem3  23094  ovolicc2lem4  23095  ovolicc2  23097  volsup  23131  dyadmbl  23174  vitalilem2  23184  vitalilem3  23185  mbfdm  23201  ismbf  23203  ismbf3d  23227  cncombf  23231  itg2seq  23315  itg2monolem2  23324  itg2monolem3  23325  itg2mono  23326  iblitg  23341  itgconst  23391  itgfsum  23399  limcvallem  23441  ellimc3  23449  cnlimci  23459  cnmptlimc  23460  dvferm1lem  23551  dvferm1  23552  dvferm2lem  23553  dvferm2  23554  dvlipcn  23561  dvle  23574  lhop1lem  23580  lhop1  23581  dvfsumge  23589  dvfsumlem2  23594  dvfsumlem3  23595  dvfsumlem4  23596  dvfsum2  23601  ftc1a  23604  ftc1lem4  23606  itgsubstlem  23615  fta1glem2  23730  fta1g  23731  plyeq0lem  23770  dgrcolem2  23834  dgrco  23835  plydivlem4  23855  plydivex  23856  fta1lem  23866  fta1  23867  vieta1lem2  23870  vieta1  23871  aalioulem2  23892  aalioulem4  23894  ulmi  23944  ulmclm  23945  ulmshftlem  23947  ulmcaulem  23952  ulmcau  23953  ulmcn  23957  ulmdvlem1  23958  ulmdvlem3  23960  ulmdv  23961  pserulm  23980  efif1olem4  24095  rlimcnp  24492  rlimcnp2  24493  xrlimcnp  24495  cxploglim  24504  scvxcvx  24512  lgamgulmlem5  24559  lgambdd  24563  wilthlem2  24595  ftalem3  24601  fsumdvdscom  24711  musumsum  24718  chtub  24737  fsumvma  24738  perfectlem2  24755  dchrelbas3  24763  dchrelbasd  24764  dchrn0  24775  dchrptlem2  24790  lgsval2lem  24832  lgsdirnn0  24869  lgsdinn0  24870  2sqlem6  24948  2sqlem10  24953  dchrisumlema  24977  dchrisumlem1  24978  dchrisumlem2  24979  dchrisumlem3  24980  dchrmusum2  24983  dchrvmasumlem2  24987  dchrvmasumlem3  24988  dchrvmasumiflem1  24990  dchrisum0flblem2  24998  dchrisum0flb  24999  dchrisum0lem1b  25004  dchrisum0lem2  25007  2vmadivsumlem  25029  chpdifbndlem1  25042  selberg3lem1  25046  selberg4lem1  25049  pntrsumbnd2  25056  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntpbnd1  25075  pntibndlem2  25080  pntibndlem3  25081  pntibnd  25082  pntlemn  25089  pntlemj  25092  pntlemi  25093  pntlemo  25096  pntlem3  25098  pntleml  25100  ostth2lem1  25107  ostth2lem2  25123  ostth3  25127  brbtwn2  25585  colinearalg  25590  axcontlem4  25647  nbgra0nb  25958  nbgrassovt  25964  cusgrarn  25988  usgrasscusgra  26011  wwlknredwwlkn  26254  wwlkextproplem2  26270  clwwlkf1  26324  clwwlkext2edg  26330  clwwisshclwwlem1  26333  clwlkf1clwwlklem  26376  nbhashnn0  26441  rusgraprop4  26471  3cyclfrgrarn1  26539  n4cyclfrgra  26545  frgrawopreglem4  26574  frgrawopreg1  26577  frgrawopreg2  26578  extwwlkfablem2  26605  isgrpo  26735  blocnilem  27043  ip2eqi  27096  ubthlem1  27110  minvecolem3  27116  htthlem  27158  hial0  27343  hial02  27344  hial2eq  27347  ocorth  27534  occllem  27546  pjhthlem1  27634  h1de2i  27796  pjjsi  27943  lnopunilem1  28253  lnophmlem1  28259  nmcexi  28269  riesz4i  28306  mdi  28538  mdbr3  28540  mdbr4  28541  dmdi  28545  dmdbr3  28548  dmdbr4  28549  dmdi4  28550  mdslmd1i  28572  atss  28589  atom1d  28596  atmd  28642  sumdmdlem2  28662  cdj1i  28676  cdj3i  28684  nn0min  28954  archiabllem1a  29076  archiabllem2a  29079  archiabl  29083  isarchiofld  29148  crefi  29242  pcmplfin  29255  fmcncfil  29305  sigaclcu  29507  unelsiga  29524  sigapildsys  29552  ldgenpisys  29556  measvun  29599  mbfmcnvima  29646  carsgclctunlem2  29708  sibfima  29727  derangenlem  30407  subfacp1lem5  30420  subfacp1lem6  30421  rescon  30482  cvmcov  30499  cvmliftlem3  30523  cvmlift2lem10  30548  cvmliftphtlem  30553  mclsax  30720  dfon2lem6  30937  poseq  30994  soseq  30995  nocvxminlem  31089  nobndlem6  31096  fwddifnp1  31442  opnrebl2  31486  nn0prpwlem  31487  nn0prpw  31488  neibastop2lem  31525  neibastop2  31526  filnetlem4  31546  fin2so  32566  poimirlem25  32604  poimirlem29  32608  poimir  32612  mbfresfi  32626  ftc1cnnclem  32653  seqpo  32713  incsequz  32714  mettrifi  32723  geomcau  32725  caushft  32727  sstotbnd2  32743  equivtotbnd  32747  totbndbnd  32758  ismtybndlem  32775  heibor1lem  32778  bfplem2  32792  opidonOLD  32821  exidu1  32825  rngoideu  32872  isdrngo2  32927  unichnidl  33000  lsat0cv  33338  lcvexchlem4  33342  lcvexchlem5  33343  eqlkr3  33406  lub0N  33494  glb0N  33498  cvrnbtwn  33576  ltrneq2  34452  trlval2  34468  lpolsatN  35795  lpolpolsatN  35796  hdmap14lem12  36189  incssnn0  36292  lnmlssfg  36668  unxpwdom3  36683  neik0pk1imk0  37365  fnchoice  38211  limcrecl  38696  fourierdlem54  39053  fourierdlem103  39102  fourierdlem104  39103  smonoord  39944  iccpartlt  39962  iccpartgt  39965  iccpartdisj  39975  fmtnodvds  39994  perfectALTVlem2  40165  bgoldbwt  40199  bgoldbst  40200  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  bgoldbnnsum3prm  40220  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbndlem4  40224  bgoldbtbnd  40225  tgblthelfgott  40229  tgoldbach  40232  tgblthelfgottOLD  40236  tgoldbachOLD  40239  reuccatpfxs1lem  40296  usgruspgrb  40411  cusgredg  40646  cusgrres  40664  usgredgsscusgredg  40675  fusgrn0degnn0  40714  1wlk1walk  40843  1wlkres  40879  1wlkp1lem6  40887  1wlkdlem2  40892  upgrwlkdvdelem  40942  pthdlem2lem  40973  lfgrn1cycl  41008  wwlksnredwwlkn  41101  wwlksnextproplem2  41116  clwwlksf1  41224  clwwlksext2edg  41230  clwwisshclwwslemlem  41233  clwlksf1clwwlklem  41275  eupth2lem3  41404  rspc2vd  41437  3cyclfrgrrn1  41455  n4cyclfrgr  41461  frgrwopreglem4  41484  frgrwopreg1  41487  frgrwopreg2  41488  av-extwwlkfablem2  41510  lcosslsp  42021  linindslinci  42031  lindslinindsimp1  42040  ldepsnlinclem1  42088  ldepsnlinclem2  42089
  Copyright terms: Public domain W3C validator