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

Theorem rspcv 3116
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
Hypothesis
Ref Expression
rspcv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspcv  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Distinct variable groups:    x, A    x, B    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem rspcv
StepHypRef Expression
1 nfv 1755 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 3114 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e. wcel 1872   A.wral 2709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ral 2714  df-v 3019
This theorem is referenced by:  rspccv  3117  rspcva  3118  rspccva  3119  rspc3v  3132  rr19.3v  3150  rr19.28v  3151  rspsbc  3316  intmin  4213  ralxfrALT  4578  somo  4746  fr2nr  4769  nvocnv  6134  weniso  6199  knatar  6202  grprinvlem  6460  grprinvd  6461  caofref  6510  fr3nr  6559  limuni3  6632  tfinds  6639  funcnvuni  6699  suppfnss  6890  onnseq  7013  smo11  7033  tfrlem1  7044  tfrlem5  7048  tfrlem9  7053  tz7.49  7112  omeulem1  7233  oeordi  7238  nneneq  7703  frfi  7764  unblem2  7772  unbnn2  7776  xpfi  7790  ordiso2  7978  ordtypelem6  7986  ordtypelem7  7987  cantnflem1c  8139  cantnflem1  8141  rankunb  8268  tcrank  8302  carduni  8362  dfac8alem  8406  acni  8422  alephinit  8472  aceq3lem  8497  dfac5  8505  dfac12lem2  8520  dfac12r  8522  dfac12k  8523  pwsdompw  8580  cflm  8626  fin1ai  8669  fin2i  8671  isfin2-2  8695  fin23lem17  8714  fin23lem39  8726  isf32lem1  8729  isf32lem2  8730  isf34lem4  8753  hsmexlem4  8805  axcc3  8814  domtriomlem  8818  axdc3lem2  8827  axdc4lem  8831  axcclem  8833  ttukeylem5  8889  ttukeylem6  8890  axdclem  8895  alephval2  8943  canth4  9018  pwfseqlem5  9034  winainflem  9064  wununi  9077  wunpw  9078  eltskm  9214  dedekind  9743  squeeze0  10455  fiminre  10501  lbreu  10502  nnsub  10594  ublbneg  11194  zsupss  11199  uzwo3  11205  zmax  11207  zbtwnre  11208  xrub  11543  infmremnf  11579  infmrp1  11580  fzrevral  11825  axdc4uzlem  12140  seqcl2  12176  seqcl  12178  seqf  12179  seqfveq2  12180  seqfveq  12182  seqshft2  12184  monoord  12188  monoord2  12189  sermono  12190  seqsplit  12191  seqcaopr3  12193  seqid  12203  seqid2  12204  seqhomo  12205  seqz  12206  discr1  12353  discr  12354  faclbnd4lem4  12426  hashbclem  12558  wrdind  12774  wrd2ind  12775  reuccats1lem  12777  recan  13338  cau3lem  13356  caubnd2  13359  limsupgre  13480  limsupgreOLD  13481  climi  13512  rlimi  13515  rlimclim1  13547  rlimclim  13548  climrlim2  13549  climshftlem  13576  rlimcld2  13580  rlimcn1  13590  climcn1  13593  subcn2  13596  isercoll  13669  isercoll2  13670  climcau  13672  caucvgrlem  13674  caucvgrlemOLD  13675  caucvgb  13684  serf0  13685  iseraltlem2  13687  iseraltlem3  13688  iseralt  13689  fsumm1  13750  fsum1p  13752  fsumcom2  13773  fsumge1  13795  telfsumo  13800  telfsumo2  13801  fsumparts  13804  o1fsum  13811  isum1p  13837  isumnn0nn  13838  isumrpcl  13839  climcndslem1  13845  climcndslem2  13846  climcnds  13847  cvgrat  13877  mertenslem1  13878  mertens  13880  clim2prod  13882  ntrivcvgfvn0  13893  fprodm1  13959  fprod1p  13960  fprodcom2  13976  sqrt2irr  14239  ndvdssub  14326  lcmf  14544  lcmfunsnlem1  14548  lcmfunsnlem2lem1  14549  lcmfunsnlem2lem2  14550  lcmfdvds  14553  lcmfdvdsb  14554  lcmfunsn  14555  prmind2  14573  nprm  14576  dvdsprm  14585  coprmgcdb  14592  coprm  14595  coprmprod  14616  coprmproddvdslem  14617  pcmpt  14775  pcmpt2  14776  pcmptdvds  14777  pcfac  14782  prmpwdvds  14786  unbenlem  14790  prmreclem4  14801  prmreclem5  14802  vdwlem1  14869  vdwlem2  14870  vdwlem9  14877  vdwlem10  14878  vdwlem13  14881  vdwnnlem1  14883  rami  14910  ramcl  14925  prmdvdsprmop  14939  prmodvdslcmf  14943  prmgaplcmlem1  14947  prmgaplcmlem1OLD  14950  prmdvdsprmorpOLD  14954  prmordvdslcmfOLD  14957  prmordvdslcmsOLDOLD  14959  prmgaplem7  14965  catidex  15518  catideu  15519  iscatd2  15525  catlid  15527  catrid  15528  subcidcl  15687  funcid  15713  initoid  15838  termoid  15839  initoeu1  15844  termoeu1  15851  yonedalem4c  16100  yonffthlem  16105  isdrs2  16122  lublecllem  16172  lubun  16307  poslubmo  16330  posglbmo  16331  sgrp2rid2ex  16599  grpidd2  16641  mulgsubcl  16710  issubg4  16774  ghmf1  16849  fislw  17215  efgi  17307  efgi2  17313  efgsdmi  17320  efgsrel  17322  gexexlem  17428  gsumzaddlem  17492  gsummhm2  17510  dprdcntz  17578  dprddisj  17579  dprdss  17600  dprd2dlem2  17611  dprd2da  17613  dpjrid  17633  ablfac1eu  17644  pgpfac1lem1  17645  pgpfaclem2  17653  srgrz  17697  srglz  17698  srgisid  17699  f1rhm0to0ALT  17907  issrngd  18027  islmodd  18035  islmhm2  18199  islbs2  18315  lbsextlem4  18322  rrgeq0i  18451  mvrf1  18587  mplsubglem  18596  mpllsslem  18597  subrgasclcl  18660  cply1mul  18825  prmirredlem  19001  ip2eq  19157  frlmphl  19276  mdetralt  19570  isclo2  20041  lmcvg  20215  cnpnei  20217  iscncl  20222  cncls  20227  lmss  20251  lmff  20254  cnt0  20299  isnrm2  20311  cnrmi  20313  isreg2  20330  cmpcov  20341  tgcmp  20353  uncmp  20355  fiuncmp  20356  dfcon2  20371  1stcclb  20396  1stcfb  20397  2ndcctbss  20407  1stcelcls  20413  restnlly  20434  islly2  20436  lly1stc  20448  comppfsc  20484  kgeni  20489  kgencn2  20509  ptpjpre1  20523  ptbasfi  20533  ptpjopn  20564  dfac14  20570  txtube  20592  txlm  20600  cnmpt11  20615  cnmpt21  20623  cnmptkp  20632  cnmptk1p  20637  qtopomap  20670  qtopcmap  20671  kqfvima  20682  kqt0lem  20688  isr0  20689  nrmr0reg  20701  fgss2  20826  isufil2  20860  cfinufil  20880  flimopn  20927  fbflim2  20929  flimcf  20934  flfneii  20944  cnpflf  20953  fclssscls  20970  fclsnei  20971  fclsrest  20976  fclscf  20977  flimfnfcls  20980  fclscmp  20982  isfcf  20986  fcfnei  20987  alexsubALTlem3  21001  alexsubALTlem4  21002  alexsubALT  21003  ptcmplem3  21006  tgpt0  21070  tsmsi  21085  tsmsgsum  21090  tsmsres  21095  tsmsxplem1  21104  tsmsxplem2  21105  tsmsxp  21106  ustincl  21159  ustdiag  21160  ustinvel  21161  ustexhalf  21162  ucnima  21233  ucncn  21237  cfiluexsm  21242  psmet0  21261  imasdsf1olem  21325  prdsbl  21443  metss  21460  comet  21465  metcnp3  21492  isngp4  21562  nmoi  21670  nmoiOLD  21686  mulc1cncf  21874  cncfco  21876  cnheiborlem  21919  cnheibor  21920  bndth  21923  lebnumii  21934  nmoleub2lem2  22067  nmoleub3  22070  ipcau2  22145  tchcphlem1  22146  tchcphlem2  22147  lmmcvg  22168  iscfil3  22180  iscau2  22184  iscau4  22186  cmetcaulem  22195  iscmet3lem1  22198  iscmet3lem2  22199  equivcfil  22206  equivcau  22207  lmcau  22219  pjthlem1  22328  pjthlem2  22329  ivthlem1  22339  ivthlem2  22340  ivthlem3  22341  ivth2  22343  ivthle  22344  ivthle2  22345  ivthicc  22346  ovoliunlem1  22392  ovolshftlem1  22399  ovolscalem1  22403  ovolicc2lem3  22409  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  ovolicc2  22413  volsup  22446  dyadmbl  22495  vitalilem2  22504  vitalilem3  22505  mbfdm  22521  ismbf  22523  ismbf3d  22547  cncombf  22551  itg2seq  22637  itg2monolem2  22646  itg2monolem3  22647  itg2mono  22648  iblitg  22663  itgconst  22713  itgfsum  22721  limcvallem  22763  ellimc3  22771  cnlimci  22781  cnmptlimc  22782  dvferm1lem  22873  dvferm1  22874  dvferm2lem  22875  dvferm2  22876  dvlipcn  22883  dvle  22896  lhop1lem  22902  lhop1  22903  dvfsumge  22911  dvfsumlem2  22916  dvfsumlem3  22917  dvfsumlem4  22918  dvfsum2  22923  ftc1a  22926  ftc1lem4  22928  itgsubstlem  22937  fta1glem2  23054  fta1g  23055  plyeq0lem  23101  dgrcolem2  23165  dgrco  23166  plydivlem4  23186  plydivex  23187  fta1lem  23197  fta1  23198  vieta1lem2  23201  vieta1  23202  aalioulem2  23226  aalioulem4  23228  tayl0  23254  ulmi  23278  ulmclm  23279  ulmshftlem  23281  ulmcaulem  23286  ulmcau  23287  ulmcn  23291  ulmdvlem1  23292  ulmdvlem3  23294  ulmdv  23295  pserulm  23314  efif1olem4  23431  rlimcnp  23828  rlimcnp2  23829  xrlimcnp  23831  cxploglim  23840  scvxcvx  23848  lgamgulmlem5  23895  lgambdd  23899  lgamcvglem  23902  wilthlem2  23931  ftalem3  23936  fsumdvdscom  24051  musumsum  24058  chtub  24077  fsumvma  24078  perfectlem2  24095  dchrelbas3  24103  dchrelbasd  24104  dchrn0  24115  dchrptlem2  24130  lgsval2lem  24171  lgsdirnn0  24204  lgsdinn0  24205  2sqlem6  24234  2sqlem10  24239  dchrisumlema  24263  dchrisumlem1  24264  dchrisumlem2  24265  dchrisumlem3  24266  dchrmusum2  24269  dchrvmasumlem2  24273  dchrvmasumlem3  24274  dchrvmasumiflem1  24276  dchrisum0flblem2  24284  dchrisum0flb  24285  dchrisum0lem1b  24290  dchrisum0lem2  24293  2vmadivsumlem  24315  chpdifbndlem1  24328  selberg3lem1  24332  selberg4lem1  24335  pntrsumbnd2  24342  pntrlog2bndlem2  24353  pntrlog2bndlem3  24354  pntrlog2bndlem5  24356  pntrlog2bndlem6  24358  pntpbnd1  24361  pntibndlem2  24366  pntibndlem3  24367  pntibnd  24368  pntlemn  24375  pntlemj  24378  pntlemi  24379  pntlemo  24382  pntlem3  24384  pntleml  24386  ostth2lem1  24393  ostth2lem2  24409  ostth3  24413  brbtwn2  24872  colinearalg  24877  axcontlem4  24934  nbgra0nb  25094  nbgrassovt  25100  cusgrarn  25124  usgrasscusgra  25148  wwlknredwwlkn  25391  wwlkextproplem2  25407  clwwlkf1  25461  clwwlkext2edg  25467  clwwisshclwwlem1  25470  clwlkf1clwwlklem  25514  nbhashnn0  25579  rusgraprop4  25609  3cyclfrgrarn1  25677  n4cyclfrgra  25683  frgrawopreglem4  25712  frgrawopreg1  25715  frgrawopreg2  25716  extwwlkfablem2  25743  isgrpo  25861  isgrp2d  25900  opidonOLD  25987  exidu1  25991  rngoideu  26049  blocnilem  26382  ip2eqi  26435  ubthlem1  26449  minvecolem3  26455  minvecolem3OLD  26465  htthlem  26507  hial0  26692  hial02  26693  hial2eq  26696  ocorth  26881  occllem  26893  pjhthlem1  26981  h1de2i  27143  pjjsi  27290  lnopunilem1  27600  lnophmlem1  27606  nmcexi  27616  riesz4i  27653  mdi  27885  mdbr3  27887  mdbr4  27888  dmdi  27892  dmdbr3  27895  dmdbr4  27896  dmdi4  27897  mdslmd1i  27919  atss  27936  atom1d  27943  atmd  27989  sumdmdlem2  28009  cdj1i  28023  cdj3i  28031  nn0min  28330  archiabllem1a  28454  archiabllem2a  28457  archiabl  28461  isarchiofld  28527  crefi  28621  pcmplfin  28634  fmcncfil  28684  sigaclcu  28886  unelsiga  28903  sigapildsys  28931  ldgenpisys  28935  measvun  28978  mbfmcnvima  29026  carsgclctunlem2  29098  sibfima  29118  derangenlem  29841  subfacp1lem5  29854  subfacp1lem6  29855  rescon  29916  cvmcov  29933  cvmliftlem3  29957  cvmlift2lem10  29982  cvmliftphtlem  29987  mclsax  30154  ghomgrpilem1  30250  ghomf1olem  30259  dfon2lem6  30380  poseq  30437  soseq  30438  nocvxminlem  30523  nobndlem6  30530  fwddifnp1  30876  opnrebl2  30921  nn0prpwlem  30922  nn0prpw  30923  neibastop2lem  30960  neibastop2  30961  filnetlem4  30981  fin2so  31839  poimirlem25  31872  poimirlem29  31876  poimir  31880  mbfresfi  31894  ftc1cnnclem  31922  seqpo  31983  incsequz  31984  mettrifi  31993  geomcau  31995  caushft  31997  sstotbnd2  32013  equivtotbnd  32017  totbndbnd  32028  ismtybndlem  32045  heibor1lem  32048  bfplem2  32062  isdrngo2  32104  unichnidl  32171  lsat0cv  32511  lcvexchlem4  32515  lcvexchlem5  32516  eqlkr3  32579  lub0N  32667  glb0N  32671  cvrnbtwn  32749  ltrneq2  33625  trlval2  33641  lpolsatN  34968  lpolpolsatN  34969  hdmap14lem12  35362  incssnn0  35465  lnmlssfg  35851  unxpwdom3  35866  fnchoice  37266  limcrecl  37592  fourierdlem54  37907  fourierdlem103  37956  fourierdlem104  37957  smonoord  38531  iccpartlt  38551  iccpartgt  38554  iccpartdisj  38564  perfectALTVlem2  38657  bgoldbwt  38691  bgoldbst  38692  nnsum4primesodd  38704  nnsum4primesoddALTV  38705  bgoldbnnsum3prm  38712  bgoldbtbndlem2  38714  bgoldbtbndlem3  38715  bgoldbtbndlem4  38716  bgoldbtbnd  38717  tgblthelfgott  38721  tgoldbach  38724  reuccatpfxs1lem  38787  usgruspgrb  39024  cusgredg  39220  cusgrres  39237  usgredgsscusgredg  39248  lcosslsp  39824  linindslinci  39834  lindslinindsimp1  39843  ldepsnlinclem1  39891  ldepsnlinclem2  39892
  Copyright terms: Public domain W3C validator