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

Theorem rspcv 3049
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 1630 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 3047 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653    e. wcel 1726   A.wral 2706
This theorem is referenced by:  rspccv  3050  rspcva  3051  rspccva  3052  rspc3v  3062  rr19.3v  3078  rr19.28v  3079  rspsbc  3240  intmin  4071  somo  4538  fr2nr  4561  ralxfrALT  4743  fr3nr  4761  limuni3  4833  tfinds  4840  funcnvuni  5519  weniso  6076  knatar  6081  grprinvlem  6286  grprinvd  6287  caofref  6331  onnseq  6607  smo11  6627  tfrlem2  6638  tfrlem9  6647  tz7.49  6703  omeulem1  6826  oeordi  6831  nneneq  7291  frfi  7353  unblem2  7361  unbnn2  7365  xpfi  7379  ordiso2  7485  ordtypelem6  7493  ordtypelem7  7494  cantnflem1c  7644  cantnflem1  7646  rankunb  7777  tcrank  7809  carduni  7869  dfac8alem  7911  acni  7927  alephinit  7977  aceq3lem  8002  dfac5  8010  dfac12lem2  8025  dfac12r  8027  dfac12k  8028  pwsdompw  8085  cflm  8131  fin1ai  8174  fin2i  8176  isfin2-2  8200  fin23lem17  8219  fin23lem39  8231  isf32lem1  8234  isf32lem2  8235  isf34lem4  8258  hsmexlem4  8310  axcc3  8319  domtriomlem  8323  axdc3lem2  8332  axdc4lem  8336  axcclem  8338  ttukeylem5  8394  ttukeylem6  8395  axdclem  8400  alephval2  8448  canth4  8523  pwfseqlem5  8539  winainflem  8569  wununi  8582  wunpw  8583  eltskm  8719  squeeze0  9914  lbreu  9959  nnsub  10039  ublbneg  10561  zsupss  10566  uzwo3  10570  zmax  10572  zbtwnre  10573  xrub  10891  fzrevral  11132  axdc4uzlem  11322  seqcl2  11342  seqcl  11344  seqf  11345  seqfveq2  11346  seqfveq  11348  seqshft2  11350  monoord  11354  monoord2  11355  sermono  11356  seqsplit  11357  seqcaopr3  11359  seqid  11369  seqid2  11370  seqhomo  11371  seqz  11372  discr1  11516  discr  11517  faclbnd4lem4  11588  hashbclem  11702  wrdind  11792  recan  12141  cau3lem  12159  caubnd2  12162  limsupgre  12276  climi  12305  rlimi  12308  rlimclim1  12340  rlimclim  12341  climrlim2  12342  climshftlem  12369  rlimcld2  12373  rlimcn1  12383  climcn1  12386  subcn2  12389  isercoll  12462  isercoll2  12463  climcau  12465  caucvgrlem  12467  caucvgb  12474  serf0  12475  iseraltlem2  12477  iseraltlem3  12478  iseralt  12479  fsumm1  12538  fsum1p  12540  fsumcom2  12559  fsumge1  12577  fsumtscopo  12582  fsumtscopo2  12583  fsumparts  12586  o1fsum  12593  isum1p  12622  isumnn0nn  12623  isumrpcl  12624  climcndslem1  12630  climcndslem2  12631  climcnds  12632  cvgrat  12661  mertenslem1  12662  mertens  12664  sqr2irr  12849  ndvdssub  12928  prmind2  13091  nprm  13094  dvdsprm  13100  coprm  13101  pcmpt  13262  pcmpt2  13263  pcmptdvds  13264  pcfac  13269  prmpwdvds  13273  unbenlem  13277  prmreclem4  13288  prmreclem5  13289  vdwlem1  13350  vdwlem2  13351  vdwlem9  13358  vdwlem10  13359  vdwlem13  13362  vdwnnlem1  13364  rami  13384  ramcl  13398  catidex  13900  catideu  13901  iscatd2  13907  catlid  13909  catrid  13910  subcidcl  14042  funcid  14068  yonedalem4c  14375  yonffthlem  14380  isdrs2  14397  lubid  14440  lubun  14551  poslubmo  14574  spwmo  14659  grpidd2  14843  mulgsubcl  14905  issubg4  14962  ghmf1  15035  fislw  15260  efgi  15352  efgi2  15358  efgsdmi  15365  efgsrel  15367  gexexlem  15468  gsumzaddlem  15527  gsummhm2  15536  dprdcntz  15567  dprddisj  15568  dprdss  15588  dprd2dlem2  15599  dprd2da  15601  dpjrid  15621  ablfac1eu  15632  pgpfac1lem1  15633  pgpfaclem2  15641  issrngd  15950  islmodd  15957  islmhm2  16115  islbs2  16227  lbsextlem4  16234  rrgeq0i  16350  mvrf1  16490  mplsubglem  16499  mpllsslem  16500  subrgasclcl  16560  prmirredlem  16774  ip2eq  16885  isclo2  17153  lmcvg  17327  cnpnei  17329  iscncl  17334  cncls  17339  lmss  17363  lmff  17366  cnt0  17411  isnrm2  17423  cnrmi  17425  isreg2  17442  cmpcov  17453  tgcmp  17465  uncmp  17467  fiuncmp  17468  bwth  17474  dfcon2  17483  1stcclb  17508  1stcfb  17509  2ndcctbss  17519  1stcelcls  17525  restnlly  17546  islly2  17548  lly1stc  17560  kgeni  17570  kgencn2  17590  ptpjpre1  17604  ptbasfi  17614  ptpjopn  17645  dfac14  17651  txtube  17673  txlm  17681  cnmpt11  17696  cnmpt21  17704  cnmptkp  17713  cnmptk1p  17718  qtopomap  17751  qtopcmap  17752  kqfvima  17763  kqt0lem  17769  isr0  17770  nrmr0reg  17782  fgss2  17907  isufil2  17941  cfinufil  17961  flimopn  18008  fbflim2  18010  flimcf  18015  flfneii  18025  cnpflf  18034  fclssscls  18051  fclsnei  18052  fclsrest  18057  fclscf  18058  flimfnfcls  18061  fclscmp  18063  isfcf  18067  fcfnei  18068  alexsubALTlem3  18081  alexsubALTlem4  18082  alexsubALT  18083  ptcmplem3  18086  tgpt0  18149  tsmsi  18164  tsmsgsum  18169  tsmsres  18174  tsmsxplem1  18183  tsmsxplem2  18184  tsmsxp  18185  ustincl  18238  ustdiag  18239  ustinvel  18240  ustexhalf  18241  isucn2  18310  ucnima  18312  ucncn  18316  cfiluexsm  18321  psmet0  18340  imasdsf1olem  18404  prdsbl  18522  metss  18539  comet  18544  metcnp3  18571  isngp4  18659  nmoi  18763  mulc1cncf  18936  cncfco  18938  cnheiborlem  18980  cnheibor  18981  bndth  18984  lebnumii  18992  nmoleub2lem2  19125  nmoleub3  19128  ipcau2  19192  tchcphlem1  19193  tchcphlem2  19194  lmmcvg  19215  iscfil3  19227  iscau2  19231  iscau4  19233  cmetcaulem  19242  iscmet3lem1  19245  iscmet3lem2  19246  equivcfil  19253  equivcau  19254  lmcau  19266  pjthlem1  19339  pjthlem2  19340  ivthlem1  19349  ivthlem2  19350  ivthlem3  19351  ivth2  19353  ivthle  19354  ivthle2  19355  ivthicc  19356  ovoliunlem1  19399  ovolshftlem1  19406  ovolscalem1  19410  ovolicc2lem3  19416  ovolicc2lem4  19417  ovolicc2  19419  volsup  19451  dyadmbl  19493  vitalilem2  19502  vitalilem3  19503  mbfdm  19521  ismbf  19523  ismbf3d  19547  cncombf  19551  itg2seq  19635  itg2monolem2  19644  itg2monolem3  19645  itg2mono  19646  iblitg  19661  itgconst  19711  itgfsum  19719  limcvallem  19759  ellimc3  19767  cnlimci  19777  cnmptlimc  19778  dvferm1lem  19869  dvferm1  19870  dvferm2lem  19871  dvferm2  19872  dvlipcn  19879  dvle  19892  lhop1lem  19898  lhop1  19899  dvfsumge  19907  dvfsumlem2  19912  dvfsumlem3  19913  dvfsumlem4  19914  dvfsum2  19919  ftc1a  19922  ftc1lem4  19924  itgsubstlem  19933  fta1glem2  20090  fta1g  20091  plyeq0lem  20130  dgrcolem2  20193  dgrco  20194  plydivlem4  20214  plydivex  20215  fta1lem  20225  fta1  20226  vieta1lem2  20229  vieta1  20230  aalioulem2  20251  aalioulem4  20253  tayl0  20279  ulmi  20303  ulmclm  20304  ulmshftlem  20306  ulmcaulem  20311  ulmcau  20312  ulmcn  20316  ulmdvlem1  20317  ulmdvlem3  20319  ulmdv  20320  pserulm  20339  efif1olem4  20448  rlimcnp  20805  rlimcnp2  20806  xrlimcnp  20808  cxploglim  20817  scvxcvx  20825  wilthlem2  20853  ftalem3  20858  fsumdvdscom  20971  musumsum  20978  chtub  20997  fsumvma  20998  perfectlem2  21015  dchrelbas3  21023  dchrelbasd  21024  dchrn0  21035  dchrptlem2  21050  lgsval2lem  21091  lgsdirnn0  21124  lgsdinn0  21125  2sqlem6  21154  2sqlem10  21159  dchrisumlema  21183  dchrisumlem1  21184  dchrisumlem2  21185  dchrisumlem3  21186  dchrmusum2  21189  dchrvmasumlem2  21193  dchrvmasumlem3  21194  dchrvmasumiflem1  21196  dchrisum0flblem2  21204  dchrisum0flb  21205  dchrisum0lem1b  21210  dchrisum0lem2  21213  2vmadivsumlem  21235  chpdifbndlem1  21248  selberg3lem1  21252  selberg4lem1  21255  pntrsumbnd2  21262  pntrlog2bndlem2  21273  pntrlog2bndlem3  21274  pntrlog2bndlem5  21276  pntrlog2bndlem6  21278  pntpbnd1  21281  pntibndlem2  21286  pntibndlem3  21287  pntibnd  21288  pntlemn  21295  pntlemj  21298  pntlemi  21299  pntlemo  21302  pntlem3  21304  pntleml  21306  ostth2lem1  21313  ostth2lem2  21329  ostth3  21333  nbgra0nb  21442  nbgrassovt  21448  cusgrarn  21469  usgrasscusgra  21493  isgrpo  21785  isgrp2d  21824  opidon  21911  exidu1  21915  rngoideu  21973  blocnilem  22306  ip2eqi  22359  ubthlem1  22373  minvecolem3  22379  htthlem  22421  hial0  22605  hial02  22606  hial2eq  22609  ocorth  22794  occllem  22806  pjhthlem1  22894  h1de2i  23056  pjjsi  23203  lnopunilem1  23514  lnophmlem1  23520  nmcexi  23530  riesz4i  23567  mdi  23799  mdbr3  23801  mdbr4  23802  dmdi  23806  dmdbr3  23809  dmdbr4  23810  dmdi4  23811  mdslmd1i  23833  atss  23850  atom1d  23857  atmd  23903  sumdmdlem2  23923  cdj1i  23937  cdj3i  23945  ofldadd  24239  ofldmul  24240  fmcncfil  24318  sigaclcu  24501  unelsiga  24518  measvun  24564  mbfmcnvima  24608  sibfima  24654  lgamgulmlem5  24818  lgambdd  24822  lgamcvglem  24825  derangenlem  24858  subfacp1lem5  24871  subfacp1lem6  24872  rescon  24934  cvmcov  24951  cvmliftlem3  24975  cvmlift2lem10  25000  cvmliftphtlem  25005  ghomgrpilem1  25097  ghomf1olem  25106  dedekind  25188  clim2prod  25217  ntrivcvgfvn0  25228  fprodm1  25291  fprod1p  25292  fprodcom2  25309  dfon2lem6  25416  poseq  25529  soseq  25530  nocvxminlem  25646  nobndlem6  25653  brbtwn2  25845  colinearalg  25850  axcontlem4  25907  mbfresfi  26254  ftc1cnnclem  26279  opnrebl2  26325  nn0prpwlem  26326  nn0prpw  26327  comppfsc  26388  neibastop2lem  26390  neibastop2  26391  filnetlem4  26411  seqpo  26452  incsequz  26453  mettrifi  26464  geomcau  26466  caushft  26468  sstotbnd2  26484  equivtotbnd  26488  totbndbnd  26499  ismtybndlem  26516  heibor1lem  26519  bfplem2  26533  isdrngo2  26575  unichnidl  26642  incssnn0  26766  lnmlssfg  27156  unxpwdom3  27234  fnchoice  27677  3cyclfrgrarn1  28403  n4cyclfrgra  28409  frgrawopreglem4  28437  frgrawopreg1  28440  frgrawopreg2  28441  lubunNEW  29772  lsat0cv  29832  lcvexchlem4  29836  lcvexchlem5  29837  eqlkr3  29900  lub0N  29988  glb0N  29992  cvrnbtwn  30070  ltrneq2  30946  trlval2  30961  lpolsatN  32287  lpolpolsatN  32288  hdmap14lem12  32681
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2711  df-v 2959
  Copyright terms: Public domain W3C validator