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

Theorem rspcv 2893
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 1609 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 2891 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632    e. wcel 1696   A.wral 2556
This theorem is referenced by:  rspccv  2894  rspcva  2895  rspccva  2896  rspc3v  2906  rr19.3v  2922  rr19.28v  2923  rspsbc  3082  intmin  3898  somo  4364  fr2nr  4387  ralxfrALT  4569  fr3nr  4587  limuni3  4659  tfinds  4666  funcnvuni  5333  weniso  5868  knatar  5873  grprinvlem  6074  grprinvd  6075  caofref  6119  onnseq  6377  smo11  6397  tfrlem2  6408  tfrlem9  6417  tz7.49  6473  omeulem1  6596  oeordi  6601  nneneq  7060  frfi  7118  unblem2  7126  unbnn2  7130  xpfi  7144  ordiso2  7246  ordtypelem6  7254  ordtypelem7  7255  cantnflem1c  7405  cantnflem1  7407  rankunb  7538  tcrank  7570  carduni  7630  dfac8alem  7672  acni  7688  alephinit  7738  aceq3lem  7763  dfac5  7771  dfac12lem2  7786  dfac12r  7788  dfac12k  7789  pwsdompw  7846  cflm  7892  fin1ai  7935  fin2i  7937  isfin2-2  7961  fin23lem17  7980  fin23lem39  7992  isf32lem1  7995  isf32lem2  7996  isf34lem4  8019  hsmexlem4  8071  axcc3  8080  domtriomlem  8084  axdc3lem2  8093  axdc4lem  8097  axcclem  8099  ttukeylem5  8156  ttukeylem6  8157  axdclem  8162  alephval2  8210  canth4  8285  pwfseqlem5  8301  winainflem  8331  wununi  8344  wunpw  8345  eltskm  8481  squeeze0  9675  lbreu  9720  nnsub  9800  ublbneg  10318  zsupss  10323  uzwo3  10327  zmax  10329  zbtwnre  10330  xrub  10646  fzrevral  10882  axdc4uzlem  11060  seqcl2  11080  seqcl  11082  seqf  11083  seqfveq2  11084  seqfveq  11086  seqshft2  11088  monoord  11092  monoord2  11093  sermono  11094  seqsplit  11095  seqcaopr3  11097  seqid  11107  seqid2  11108  seqhomo  11109  seqz  11110  discr1  11253  discr  11254  faclbnd4lem4  11325  hashbclem  11406  wrdind  11493  recan  11836  cau3lem  11854  caubnd2  11857  limsupgre  11971  climi  12000  rlimi  12003  rlimclim1  12035  rlimclim  12036  climrlim2  12037  climshftlem  12064  rlimcld2  12068  rlimcn1  12078  climcn1  12081  subcn2  12084  isercoll  12157  isercoll2  12158  climcau  12160  caucvgrlem  12161  caucvgb  12168  serf0  12169  iseraltlem2  12171  iseraltlem3  12172  iseralt  12173  fsumm1  12232  fsum1p  12234  fsumcom2  12253  fsumge1  12271  fsumtscopo  12276  fsumtscopo2  12277  fsumparts  12280  o1fsum  12287  isum1p  12316  isumnn0nn  12317  isumrpcl  12318  climcndslem1  12324  climcndslem2  12325  climcnds  12326  cvgrat  12355  mertenslem1  12356  mertens  12358  sqr2irr  12543  ndvdssub  12622  prmind2  12785  nprm  12788  dvdsprm  12794  coprm  12795  pcmpt  12956  pcmpt2  12957  pcmptdvds  12958  pcfac  12963  prmpwdvds  12967  unbenlem  12971  prmreclem4  12982  prmreclem5  12983  vdwlem1  13044  vdwlem2  13045  vdwlem9  13052  vdwlem10  13053  vdwlem13  13056  vdwnnlem1  13058  rami  13078  ramcl  13092  catidex  13592  catideu  13593  iscatd2  13599  catlid  13601  catrid  13602  subcidcl  13734  funcid  13760  yonedalem4c  14067  yonffthlem  14072  isdrs2  14089  lubid  14132  lubun  14243  poslubmo  14266  spwmo  14351  grpidd2  14535  mulgsubcl  14597  issubg4  14654  ghmf1  14727  fislw  14952  efgi  15044  efgi2  15050  efgsdmi  15057  efgsrel  15059  gexexlem  15160  gsumzaddlem  15219  gsummhm2  15228  dprdcntz  15259  dprddisj  15260  dprdss  15280  dprd2dlem2  15291  dprd2da  15293  dpjrid  15313  ablfac1eu  15324  pgpfac1lem1  15325  pgpfaclem2  15333  issrngd  15642  islmodd  15649  islmhm2  15811  islbs2  15923  lbsextlem4  15930  rrgeq0i  16046  mvrf1  16186  mplsubglem  16195  mpllsslem  16196  subrgasclcl  16256  prmirredlem  16462  ip2eq  16573  isclo2  16841  lmcvg  17008  cnpnei  17009  iscncl  17014  cncls  17019  lmss  17042  lmff  17045  cnt0  17090  isnrm2  17102  cnrmi  17104  isreg2  17121  cmpcov  17132  tgcmp  17144  uncmp  17146  fiuncmp  17147  dfcon2  17161  1stcclb  17186  1stcfb  17187  2ndcctbss  17197  1stcelcls  17203  restnlly  17224  islly2  17226  lly1stc  17238  kgeni  17248  kgencn2  17268  ptpjpre1  17282  ptbasfi  17292  ptpjopn  17322  dfac14  17328  txtube  17350  txlm  17358  cnmpt11  17373  cnmpt21  17381  cnmptkp  17390  cnmptk1p  17395  qtopomap  17425  qtopcmap  17426  kqfvima  17437  kqt0lem  17443  isr0  17444  nrmr0reg  17456  fgss2  17585  isufil2  17619  cfinufil  17639  flimopn  17686  fbflim2  17688  flimcf  17693  flfneii  17703  cnpflf  17712  fclssscls  17729  fclsnei  17730  fclsrest  17735  fclscf  17736  flimfnfcls  17739  fclscmp  17741  isfcf  17745  fcfnei  17746  alexsubALTlem3  17759  alexsubALTlem4  17760  alexsubALT  17761  ptcmplem3  17764  tgpt0  17817  tsmsi  17832  tsmsgsum  17837  tsmsres  17842  tsmsxplem1  17851  tsmsxplem2  17852  tsmsxp  17853  imasdsf1olem  17953  prdsbl  18053  metss  18070  comet  18075  metcnp3  18102  isngp4  18149  nmoi  18253  mulc1cncf  18425  cncfco  18427  cnheiborlem  18468  cnheibor  18469  bndth  18472  lebnumii  18480  nmoleub2lem2  18613  nmoleub3  18616  ipcau2  18680  tchcphlem1  18681  tchcphlem2  18682  lmmcvg  18703  iscfil3  18715  iscau2  18719  iscau4  18721  cmetcaulem  18730  iscmet3lem1  18733  iscmet3lem2  18734  equivcfil  18741  equivcau  18742  lmcau  18754  pjthlem1  18817  pjthlem2  18818  ivthlem1  18827  ivthlem2  18828  ivthlem3  18829  ivth2  18831  ivthle  18832  ivthle2  18833  ivthicc  18834  ovoliunlem1  18877  ovolshftlem1  18884  ovolscalem1  18888  ovolicc2lem3  18894  ovolicc2lem4  18895  ovolicc2  18897  volsup  18929  dyadmbl  18971  vitalilem2  18980  vitalilem3  18981  mbfdm  18999  ismbf  19001  ismbf3d  19025  cncombf  19029  itg2seq  19113  itg2monolem2  19122  itg2monolem3  19123  itg2mono  19124  iblitg  19139  itgconst  19189  itgfsum  19197  limcvallem  19237  ellimc3  19245  cnlimci  19255  cnmptlimc  19256  dvferm1lem  19347  dvferm1  19348  dvferm2lem  19349  dvferm2  19350  dvlipcn  19357  dvle  19370  lhop1lem  19376  lhop1  19377  dvfsumge  19385  dvfsumlem2  19390  dvfsumlem3  19391  dvfsumlem4  19392  dvfsum2  19397  ftc1a  19400  ftc1lem4  19402  itgsubstlem  19411  fta1glem2  19568  fta1g  19569  plyeq0lem  19608  dgrcolem2  19671  dgrco  19672  plydivlem4  19692  plydivex  19693  fta1lem  19703  fta1  19704  vieta1lem2  19707  vieta1  19708  aalioulem2  19729  aalioulem4  19731  tayl0  19757  ulmi  19781  ulmclm  19782  ulmshftlem  19784  ulmcaulem  19787  ulmcau  19788  ulmcn  19792  ulmdvlem1  19793  ulmdvlem3  19795  ulmdv  19796  pserulm  19814  efif1olem4  19923  rlimcnp  20276  rlimcnp2  20277  xrlimcnp  20279  cxploglim  20288  scvxcvx  20296  wilthlem2  20323  ftalem3  20328  fsumdvdscom  20441  musumsum  20448  chtub  20467  fsumvma  20468  perfectlem2  20485  dchrelbas3  20493  dchrelbasd  20494  dchrn0  20505  dchrptlem2  20520  lgsval2lem  20561  lgsdirnn0  20594  lgsdinn0  20595  2sqlem6  20624  2sqlem10  20629  dchrisumlema  20653  dchrisumlem1  20654  dchrisumlem2  20655  dchrisumlem3  20656  dchrmusum2  20659  dchrvmasumlem2  20663  dchrvmasumlem3  20664  dchrvmasumiflem1  20666  dchrisum0flblem2  20674  dchrisum0flb  20675  dchrisum0lem1b  20680  dchrisum0lem2  20683  2vmadivsumlem  20705  chpdifbndlem1  20718  selberg3lem1  20722  selberg4lem1  20725  pntrsumbnd2  20732  pntrlog2bndlem2  20743  pntrlog2bndlem3  20744  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntpbnd1  20751  pntibndlem2  20756  pntibndlem3  20757  pntibnd  20758  pntlemn  20765  pntlemj  20768  pntlemi  20769  pntlemo  20772  pntlem3  20774  pntleml  20776  ostth2lem1  20783  ostth2lem2  20799  ostth3  20803  isgrpo  20879  isgrp2d  20918  opidon  21005  exidu1  21009  rngoideu  21067  blocnilem  21398  ip2eqi  21451  ubthlem1  21465  minvecolem3  21471  htthlem  21513  hial0  21697  hial02  21698  hial2eq  21701  ocorth  21886  occllem  21898  pjhthlem1  21986  h1de2i  22148  pjjsi  22295  lnopunilem1  22606  lnophmlem1  22612  nmcexi  22622  riesz4i  22659  mdi  22891  mdbr3  22893  mdbr4  22894  dmdi  22898  dmdbr3  22901  dmdbr4  22902  dmdi4  22903  mdslmd1i  22925  atss  22942  atom1d  22949  atmd  22995  sumdmdlem2  23015  cdj1i  23029  cdj3i  23037  sigaclcu  23493  unelsiga  23510  measvun  23552  mbfmcnvima  23577  derangenlem  23717  subfacp1lem5  23730  subfacp1lem6  23731  rescon  23792  cvmcov  23809  cvmliftlem3  23833  cvmlift2lem10  23858  cvmliftphtlem  23863  ghomgrpilem1  24007  ghomf1olem  24016  dedekind  24097  dfon2lem6  24215  poseq  24324  soseq  24325  nocvxminlem  24415  nobndlem6  24422  brbtwn2  24605  colinearalg  24610  axcontlem4  24667  ftc1cnnclem  25024  dstr  25274  supdefa  25366  ridlideq  25438  basexre  25625  osneisi  25634  exopcopn  25675  limptlimpr2lem2  25678  bwt2  25695  supnuf  25732  pgapspf  26155  pgapspf2  26156  elhaltdp2  26171  tethpnc2  26174  isibg2aa  26215  isibg2aalem2  26217  isibg2aalem3  26218  opnrebl2  26339  nn0prpwlem  26341  nn0prpw  26342  comppfsc  26410  neibastop2lem  26412  neibastop2  26413  filnetlem4  26433  seqpo  26560  incsequz  26561  mettrifi  26576  geomcau  26578  caushft  26580  sstotbnd2  26601  equivtotbnd  26605  totbndbnd  26616  ismtybndlem  26633  heibor1lem  26636  bfplem2  26650  isdrngo2  26692  unichnidl  26759  incssnn0  26889  lnmlssfg  27281  unxpwdom3  27359  fnchoice  27803  nbgra0nb  28278  nbgrassovt  28284  3cyclfrgrarn1  28435  n4cyclfrgra  28440  lubunNEW  29785  lsat0cv  29845  lcvexchlem4  29849  lcvexchlem5  29850  eqlkr3  29913  lub0N  30001  glb0N  30005  cvrnbtwn  30083  ltrneq2  30959  trlval2  30974  lpolsatN  32300  lpolpolsatN  32301  hdmap14lem12  32694
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803
  Copyright terms: Public domain W3C validator