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

Theorem rspcv 3336
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 1883 . 2 𝑥𝜓
2 rspcv.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2rspc 3334 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233
This theorem is referenced by:  rspccv  3337  rspcva  3338  rspccva  3339  rspcda  3346  rspc3v  3356  rr19.3v  3377  rr19.28v  3378  rspsbc  3551  intmin  4529  ralxfrALT  4917  somo  5098  fr2nr  5121  nvocnv  6577  weniso  6644  knatar  6647  caofref  6965  fr3nr  7021  limuni3  7094  tfinds  7101  funcnvuni  7161  suppfnss  7365  onnseq  7486  smo11  7506  tfrlem1  7517  tfrlem5  7521  tfrlem9  7526  tz7.49  7585  omeulem1  7707  oeordi  7712  nneneq  8184  frfi  8246  unblem2  8254  unbnn2  8258  xpfi  8272  ordiso2  8461  ordtypelem6  8469  ordtypelem7  8470  cantnflem1c  8622  cantnflem1  8624  rankunb  8751  tcrank  8785  carduni  8845  dfac8alem  8890  acni  8906  alephinit  8956  aceq3lem  8981  dfac5  8989  dfac12lem2  9004  dfac12r  9006  dfac12k  9007  pwsdompw  9064  cflm  9110  fin2i  9155  isfin2-2  9179  fin23lem17  9198  fin23lem39  9210  isf32lem1  9213  isf32lem2  9214  isf34lem4  9237  hsmexlem4  9289  axcc3  9298  domtriomlem  9302  axdc3lem2  9311  axdc4lem  9315  axcclem  9317  ttukeylem5  9373  ttukeylem6  9374  axdclem  9379  alephval2  9432  canth4  9507  pwfseqlem5  9523  winainflem  9553  wununi  9566  wunpw  9567  eltskm  9703  dedekind  10238  squeeze0  10964  fiminre  11010  lbreu  11011  nnsub  11097  ublbneg  11811  zsupss  11815  uzwo3  11821  zmax  11823  zbtwnre  11824  xrub  12180  infmremnf  12211  infmrp1  12212  fzrevral  12463  axdc4uzlem  12822  seqcl2  12859  seqcl  12861  seqf  12862  seqfveq2  12863  seqfveq  12865  monoord  12871  monoord2  12872  sermono  12873  seqcaopr3  12876  seqid  12886  seqid2  12887  seqhomo  12888  seqz  12889  discr1  13040  discr  13041  faclbnd4lem4  13123  hashbclem  13274  ccatalpha  13411  wrdind  13522  wrd2ind  13523  reuccats1lem  13525  recan  14120  cau3lem  14138  caubnd2  14141  limsupgre  14256  climi  14285  rlimi  14288  rlimclim1  14320  rlimclim  14321  climrlim2  14322  climshftlem  14349  rlimcld2  14353  rlimcn1  14363  climcn1  14366  subcn2  14369  isercoll  14442  isercoll2  14443  climcau  14445  caucvgrlem  14447  caucvgb  14454  serf0  14455  iseraltlem2  14457  iseraltlem3  14458  iseralt  14459  fsumm1  14524  fsum1p  14526  fsumcom2  14549  fsumcom2OLD  14550  fsumge1  14573  telfsumo  14578  telfsumo2  14579  fsumparts  14582  o1fsum  14589  isum1p  14617  isumnn0nn  14618  isumrpcl  14619  climcndslem1  14625  climcndslem2  14626  climcnds  14627  cvgrat  14659  mertenslem1  14660  mertens  14662  clim2prod  14664  ntrivcvgfvn0  14675  fprodm1  14741  fprod1p  14742  fprodcom2  14758  fprodcom2OLD  14759  sqrt2irr  15023  ndvdssub  15180  dfgcd2  15310  lcmf  15393  lcmfunsnlem1  15397  lcmfunsnlem2lem1  15398  lcmfunsnlem2lem2  15399  lcmfdvds  15402  lcmfdvdsb  15403  lcmfunsn  15404  coprmgcdb  15409  coprmdvds1  15412  coprmprod  15422  coprmproddvdslem  15423  prmind2  15445  nprm  15448  dvdsprm  15462  coprm  15470  pcmpt  15643  pcmpt2  15644  pcmptdvds  15645  pcfac  15650  prmpwdvds  15655  unbenlem  15659  prmreclem4  15670  vdwlem1  15732  vdwlem2  15733  vdwlem9  15740  vdwlem10  15741  vdwlem13  15744  vdwnnlem1  15746  rami  15766  ramcl  15780  prmdvdsprmop  15794  prmodvdslcmf  15798  prmgaplcmlem1  15802  prmgaplem7  15808  catidex  16382  catideu  16383  iscatd2  16389  catlid  16391  catrid  16392  subcidcl  16551  funcid  16577  initoid  16702  termoid  16703  initoeu1  16708  termoeu1  16715  yonedalem4c  16964  yonffthlem  16969  isdrs2  16986  lublecllem  17035  lubun  17170  poslubmo  17193  posglbmo  17194  sgrp2rid2ex  17461  dfgrp2  17494  grpidd2  17506  grpidinv2  17521  dfgrp3lem  17560  mulgsubcl  17602  issubg4  17660  ghmf1  17736  fislw  18086  efgi  18178  efgi2  18184  efgsdmi  18191  efgsrel  18193  gexexlem  18301  gsummhm2  18385  dprdcntz  18453  dprddisj  18454  dprdss  18474  dprd2dlem2  18485  dprd2da  18487  dpjrid  18507  pgpfac1lem1  18519  pgpfaclem2  18527  srgrz  18572  srglz  18573  srgisid  18574  f1rhm0to0ALT  18789  issrngd  18909  islmodd  18917  rmodislmod  18979  islmhm2  19086  islbs2  19202  lbsextlem4  19209  rrgeq0i  19337  mvrf1  19473  mplsubglem  19482  mpllsslem  19483  subrgasclcl  19547  cply1mul  19712  prmirredlem  19889  ip2eq  20046  frlmphl  20168  mdetralt  20462  isclo2  20940  lmcvg  21114  cnpnei  21116  iscncl  21121  cncls  21126  lmss  21150  lmff  21153  cnt0  21198  isnrm2  21210  cnrmi  21212  isreg2  21229  tgcmp  21252  uncmp  21254  fiuncmp  21255  dfconn2  21270  1stcclb  21295  1stcfb  21296  2ndcctbss  21306  1stcelcls  21312  restnlly  21333  islly2  21335  lly1stc  21347  comppfsc  21383  kgeni  21388  kgencn2  21408  ptpjpre1  21422  ptbasfi  21432  ptpjopn  21463  dfac14  21469  txtube  21491  txlm  21499  cnmpt11  21514  cnmpt21  21522  cnmptkp  21531  cnmptk1p  21536  qtopomap  21569  qtopcmap  21570  kqfvima  21581  kqt0lem  21587  isr0  21588  nrmr0reg  21600  fgss2  21725  isufil2  21759  cfinufil  21779  flimopn  21826  fbflim2  21828  flimcf  21833  flfneii  21843  cnpflf  21852  fclssscls  21869  fclsnei  21870  fclsrest  21875  fclscf  21876  flimfnfcls  21879  fclscmp  21881  isfcf  21885  fcfnei  21886  alexsubALTlem3  21900  alexsubALTlem4  21901  alexsubALT  21902  ptcmplem3  21905  tgpt0  21969  tsmsi  21984  tsmsgsum  21989  tsmsres  21994  tsmsxplem1  22003  tsmsxplem2  22004  tsmsxp  22005  ustincl  22058  ustdiag  22059  ustinvel  22060  ustexhalf  22061  ucnima  22132  ucncn  22136  cfiluexsm  22141  psmet0  22160  imasdsf1olem  22225  prdsbl  22343  metss  22360  comet  22365  metcnp3  22392  isngp4  22463  nmoi  22579  mulc1cncf  22755  cncfco  22757  cnheiborlem  22800  cnheibor  22801  bndth  22804  lebnumii  22812  nmoleub2lem2  22962  nmoleub3  22965  ipcau2  23079  tchcphlem1  23080  tchcphlem2  23081  lmmcvg  23105  iscfil3  23117  iscau2  23121  iscau4  23123  cmetcaulem  23132  iscmet3lem1  23135  iscmet3lem2  23136  equivcfil  23143  equivcau  23144  lmcau  23157  pjthlem1  23254  pjthlem2  23255  ivthlem1  23266  ivthlem2  23267  ivthlem3  23268  ivth2  23270  ivthle  23271  ivthle2  23272  ivthicc  23273  ovoliunlem1  23316  ovolshftlem1  23323  ovolscalem1  23327  ovolicc2lem3  23333  ovolicc2lem4  23334  ovolicc2  23336  volsup  23370  dyadmbl  23414  vitalilem2  23423  vitalilem3  23424  mbfdm  23440  ismbf  23442  ismbf3d  23466  cncombf  23470  itg2seq  23554  itg2monolem2  23563  itg2monolem3  23564  itg2mono  23565  iblitg  23580  itgconst  23630  itgfsum  23638  limcvallem  23680  ellimc3  23688  cnlimci  23698  cnmptlimc  23699  dvferm1lem  23792  dvferm1  23793  dvferm2lem  23794  dvferm2  23795  dvlipcn  23802  dvle  23815  lhop1lem  23821  lhop1  23822  dvfsumge  23830  dvfsumlem2  23835  dvfsumlem3  23836  dvfsumlem4  23837  dvfsum2  23842  ftc1a  23845  ftc1lem4  23847  itgsubstlem  23856  fta1glem2  23971  fta1g  23972  plyeq0lem  24011  dgrcolem2  24075  dgrco  24076  plydivlem4  24096  plydivex  24097  fta1lem  24107  fta1  24108  vieta1lem2  24111  vieta1  24112  aalioulem2  24133  aalioulem4  24135  ulmi  24185  ulmclm  24186  ulmshftlem  24188  ulmcaulem  24193  ulmcau  24194  ulmcn  24198  ulmdvlem1  24199  ulmdvlem3  24201  ulmdv  24202  pserulm  24221  efif1olem4  24336  rlimcnp  24737  rlimcnp2  24738  xrlimcnp  24740  cxploglim  24749  scvxcvx  24757  lgamgulmlem5  24804  lgambdd  24808  wilthlem2  24840  ftalem3  24846  fsumdvdscom  24956  musumsum  24963  chtub  24982  fsumvma  24983  perfectlem2  25000  dchrelbas3  25008  dchrelbasd  25009  dchrn0  25020  dchrptlem2  25035  lgsval2lem  25077  lgsdirnn0  25114  lgsdinn0  25115  2sqlem6  25193  2sqlem10  25198  dchrisumlema  25222  dchrisumlem1  25223  dchrisumlem2  25224  dchrisumlem3  25225  dchrmusum2  25228  dchrvmasumlem2  25232  dchrvmasumlem3  25233  dchrvmasumiflem1  25235  dchrisum0flblem2  25243  dchrisum0flb  25244  dchrisum0lem1b  25249  dchrisum0lem2  25252  2vmadivsumlem  25274  chpdifbndlem1  25287  selberg3lem1  25291  selberg4lem1  25294  pntrsumbnd2  25301  pntrlog2bndlem2  25312  pntrlog2bndlem3  25313  pntrlog2bndlem5  25315  pntrlog2bndlem6  25317  pntpbnd1  25320  pntibndlem2  25325  pntibndlem3  25326  pntibnd  25327  pntlemn  25334  pntlemj  25337  pntlemi  25338  pntlemo  25341  pntlem3  25343  pntleml  25345  ostth2lem1  25352  ostth2lem2  25368  ostth3  25372  brbtwn2  25830  colinearalg  25835  axcontlem4  25892  usgruspgrb  26121  cusgredg  26376  cusgrres  26400  usgredgsscusgredg  26411  fusgrn0degnn0  26451  wlk1walk  26591  wlkres  26623  wlkp1lem6  26631  wlkdlem2  26636  upgrwlkdvdelem  26688  pthdlem2lem  26719  lfgrn1cycl  26753  wwlksnredwwlkn  26858  wwlksnextproplem2  26873  clwwisshclwwslemlem  26970  clwwlkf1  27012  clwwlkext2edg  27020  clwlksf1clwwlklem  27055  eupth2lem3  27214  rspc2vd  27245  3cyclfrgrrn1  27265  n4cyclfrgr  27271  frgrwopregasn  27296  frgrwopregbsn  27297  clwwlkccatlem  27331  isgrpo  27479  blocnilem  27787  ip2eqi  27840  ubthlem1  27854  minvecolem3  27860  htthlem  27902  hial0  28087  hial02  28088  hial2eq  28091  ocorth  28278  occllem  28290  pjhthlem1  28378  h1de2i  28540  pjjsi  28687  lnopunilem1  28997  lnophmlem1  29003  nmcexi  29013  riesz4i  29050  mdi  29282  mdbr3  29284  mdbr4  29285  dmdi  29289  dmdbr3  29292  dmdbr4  29293  dmdi4  29294  mdslmd1i  29316  atss  29333  atom1d  29340  atmd  29386  sumdmdlem2  29406  cdj1i  29420  cdj3i  29428  nn0min  29695  archiabllem1a  29873  archiabllem2a  29876  archiabl  29880  isarchiofld  29945  crefi  30042  pcmplfin  30055  fmcncfil  30105  sigaclcu  30308  unelsiga  30325  sigapildsys  30353  ldgenpisys  30357  measvun  30400  mbfmcnvima  30447  carsgclctunlem2  30509  sibfima  30528  derangenlem  31279  subfacp1lem5  31292  subfacp1lem6  31293  resconn  31354  cvmcov  31371  cvmliftlem3  31395  cvmliftphtlem  31425  mclsax  31592  dfon2lem6  31817  poseq  31878  soseq  31879  nolt02o  31970  noresle  31971  noprefixmo  31973  nosupbnd1lem1  31979  nosupbnd1lem4  31982  nosupbnd2lem1  31986  nosupbnd2  31987  nocvxminlem  32018  fwddifnp1  32397  opnrebl2  32441  nn0prpwlem  32442  nn0prpw  32443  neibastop2lem  32480  neibastop2  32481  filnetlem4  32501  bj-mooreset  33181  bj-ismoored0  33186  bj-ismoored  33187  dfgcd3  33300  fin2so  33526  poimirlem25  33564  poimirlem29  33568  poimir  33572  mbfresfi  33586  ftc1cnnclem  33613  seqpo  33673  incsequz  33674  mettrifi  33683  geomcau  33685  caushft  33687  sstotbnd2  33703  equivtotbnd  33707  totbndbnd  33718  ismtybndlem  33735  heibor1lem  33738  bfplem2  33752  opidonOLD  33781  exidu1  33785  rngoideu  33832  isdrngo2  33887  unichnidl  33960  lsat0cv  34638  lcvexchlem4  34642  lcvexchlem5  34643  eqlkr3  34706  lub0N  34794  glb0N  34798  cvrnbtwn  34876  ltrneq2  35752  trlval2  35768  lpolsatN  37094  lpolpolsatN  37095  hdmap14lem12  37488  incssnn0  37591  lnmlssfg  37967  unxpwdom3  37982  neik0pk1imk0  38662  fnchoice  39502  monoordxrv  40025  monoord2xrv  40027  limcrecl  40179  fourierdlem54  40695  fourierdlem103  40744  fourierdlem104  40745  smonoord  41666  iccpartlt  41685  iccpartgt  41688  iccpartdisj  41698  reuccatpfxs1lem  41758  fmtnodvds  41781  perfectALTVlem2  41956  sbgoldbwt  41990  sbgoldbst  41991  sgoldbeven3prm  41996  mogoldbb  41998  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  bgoldbnnsum3prm  42017  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  bgoldbtbndlem4  42021  bgoldbtbnd  42022  tgblthelfgott  42028  tgoldbach  42030  tgblthelfgottOLD  42034  tgoldbachOLD  42037  lcosslsp  42552  linindslinci  42562  lindslinindsimp1  42571  ldepsnlinclem1  42619  ldepsnlinclem2  42620
  Copyright terms: Public domain W3C validator