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

Theorem rspcv 3192
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 1694 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 3190 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1383    e. wcel 1804   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-v 3097
This theorem is referenced by:  rspccv  3193  rspcva  3194  rspccva  3195  rspc3v  3208  rr19.3v  3227  rr19.28v  3228  rspsbc  3403  intmin  4291  ralxfrALT  4656  somo  4824  fr2nr  4847  nvocnv  6172  weniso  6235  knatar  6238  grprinvlem  6498  grprinvd  6499  caofref  6551  fr3nr  6600  limuni3  6672  tfinds  6679  funcnvuni  6738  suppfnss  6927  onnseq  7017  smo11  7037  tfrlem1  7047  tfrlem5  7051  tfrlem9  7056  tz7.49  7112  omeulem1  7233  oeordi  7238  nneneq  7702  frfi  7767  unblem2  7775  unbnn2  7779  xpfi  7793  ordiso2  7943  ordtypelem6  7951  ordtypelem7  7952  cantnflem1c  8109  cantnflem1  8111  cantnflem1cOLD  8132  cantnflem1OLD  8134  rankunb  8271  tcrank  8305  carduni  8365  dfac8alem  8413  acni  8429  alephinit  8479  aceq3lem  8504  dfac5  8512  dfac12lem2  8527  dfac12r  8529  dfac12k  8530  pwsdompw  8587  cflm  8633  fin1ai  8676  fin2i  8678  isfin2-2  8702  fin23lem17  8721  fin23lem39  8733  isf32lem1  8736  isf32lem2  8737  isf34lem4  8760  hsmexlem4  8812  axcc3  8821  domtriomlem  8825  axdc3lem2  8834  axdc4lem  8838  axcclem  8840  ttukeylem5  8896  ttukeylem6  8897  axdclem  8902  alephval2  8950  canth4  9028  pwfseqlem5  9044  winainflem  9074  wununi  9087  wunpw  9088  eltskm  9224  dedekind  9747  squeeze0  10455  lbreu  10500  nnsub  10581  ublbneg  11177  zsupss  11182  uzwo3  11188  zmax  11190  zbtwnre  11191  xrub  11514  fzrevral  11774  axdc4uzlem  12074  seqcl2  12107  seqcl  12109  seqf  12110  seqfveq2  12111  seqfveq  12113  seqshft2  12115  monoord  12119  monoord2  12120  sermono  12121  seqsplit  12122  seqcaopr3  12124  seqid  12134  seqid2  12135  seqhomo  12136  seqz  12137  discr1  12284  discr  12285  faclbnd4lem4  12356  hashbclem  12483  wrdind  12684  wrd2ind  12685  reuccats1lem  12687  recan  13151  cau3lem  13169  caubnd2  13172  limsupgre  13286  climi  13315  rlimi  13318  rlimclim1  13350  rlimclim  13351  climrlim2  13352  climshftlem  13379  rlimcld2  13383  rlimcn1  13393  climcn1  13396  subcn2  13399  isercoll  13472  isercoll2  13473  climcau  13475  caucvgrlem  13477  caucvgb  13484  serf0  13485  iseraltlem2  13487  iseraltlem3  13488  iseralt  13489  fsumm1  13548  fsum1p  13550  fsumcom2  13571  fsumge1  13593  telfsumo  13598  telfsumo2  13599  fsumparts  13602  o1fsum  13609  isum1p  13635  isumnn0nn  13636  isumrpcl  13637  climcndslem1  13643  climcndslem2  13644  climcnds  13645  cvgrat  13674  mertenslem1  13675  mertens  13677  clim2prod  13679  ntrivcvgfvn0  13690  fprodm1  13753  fprod1p  13754  fprodcom2  13770  sqrt2irr  13964  ndvdssub  14047  prmind2  14210  nprm  14213  dvdsprm  14222  coprm  14223  pcmpt  14393  pcmpt2  14394  pcmptdvds  14395  pcfac  14400  prmpwdvds  14404  unbenlem  14408  prmreclem4  14419  prmreclem5  14420  vdwlem1  14481  vdwlem2  14482  vdwlem9  14489  vdwlem10  14490  vdwlem13  14493  vdwnnlem1  14495  rami  14515  ramcl  14529  catidex  15053  catideu  15054  iscatd2  15060  catlid  15062  catrid  15063  subcidcl  15192  funcid  15218  yonedalem4c  15525  yonffthlem  15530  isdrs2  15547  lublecllem  15597  lubun  15732  poslubmo  15755  posglbmo  15756  sgrp2rid2ex  16024  grpidd2  16066  mulgsubcl  16135  issubg4  16199  ghmf1  16274  fislw  16624  efgi  16716  efgi2  16722  efgsdmi  16729  efgsrel  16731  gexexlem  16837  gsumzaddlem  16913  gsumzaddlemOLD  16915  gsummhm2  16940  gsummhm2OLD  16941  dprdcntz  17020  dprddisj  17021  dprdss  17055  dprd2dlem2  17068  dprd2da  17070  dpjrid  17090  ablfac1eu  17103  pgpfac1lem1  17104  pgpfaclem2  17112  srgrz  17156  srglz  17157  srgisid  17158  f1rhm0to0ALT  17369  issrngd  17489  islmodd  17497  islmhm2  17663  islbs2  17779  lbsextlem4  17786  rrgeq0i  17916  mvrf1  18060  mplsubglem  18072  mpllsslem  18073  mplsubglemOLD  18074  mpllsslemOLD  18075  subrgasclcl  18143  cply1mul  18314  prmirredlem  18501  prmirredlemOLD  18504  ip2eq  18666  frlmphl  18790  mdetralt  19088  isclo2  19567  lmcvg  19741  cnpnei  19743  iscncl  19748  cncls  19753  lmss  19777  lmff  19780  cnt0  19825  isnrm2  19837  cnrmi  19839  isreg2  19856  cmpcov  19867  tgcmp  19879  uncmp  19881  fiuncmp  19882  bwthOLD  19889  dfcon2  19898  1stcclb  19923  1stcfb  19924  2ndcctbss  19934  1stcelcls  19940  restnlly  19961  islly2  19963  lly1stc  19975  comppfsc  20011  kgeni  20016  kgencn2  20036  ptpjpre1  20050  ptbasfi  20060  ptpjopn  20091  dfac14  20097  txtube  20119  txlm  20127  cnmpt11  20142  cnmpt21  20150  cnmptkp  20159  cnmptk1p  20164  qtopomap  20197  qtopcmap  20198  kqfvima  20209  kqt0lem  20215  isr0  20216  nrmr0reg  20228  fgss2  20353  isufil2  20387  cfinufil  20407  flimopn  20454  fbflim2  20456  flimcf  20461  flfneii  20471  cnpflf  20480  fclssscls  20497  fclsnei  20498  fclsrest  20503  fclscf  20504  flimfnfcls  20507  fclscmp  20509  isfcf  20513  fcfnei  20514  alexsubALTlem3  20527  alexsubALTlem4  20528  alexsubALT  20529  ptcmplem3  20532  tgpt0  20595  tsmsi  20610  tsmsgsum  20615  tsmsgsumOLD  20618  tsmsresOLD  20623  tsmsres  20624  tsmsxplem1  20633  tsmsxplem2  20634  tsmsxp  20635  ustincl  20688  ustdiag  20689  ustinvel  20690  ustexhalf  20691  ucnima  20762  ucncn  20766  cfiluexsm  20771  psmet0  20790  imasdsf1olem  20854  prdsbl  20972  metss  20989  comet  20994  metcnp3  21021  isngp4  21109  nmoi  21213  mulc1cncf  21387  cncfco  21389  cnheiborlem  21432  cnheibor  21433  bndth  21436  lebnumii  21444  nmoleub2lem2  21577  nmoleub3  21580  ipcau2  21655  tchcphlem1  21656  tchcphlem2  21657  lmmcvg  21678  iscfil3  21690  iscau2  21694  iscau4  21696  cmetcaulem  21705  iscmet3lem1  21708  iscmet3lem2  21709  equivcfil  21716  equivcau  21717  lmcau  21729  pjthlem1  21830  pjthlem2  21831  ivthlem1  21841  ivthlem2  21842  ivthlem3  21843  ivth2  21845  ivthle  21846  ivthle2  21847  ivthicc  21848  ovoliunlem1  21891  ovolshftlem1  21898  ovolscalem1  21902  ovolicc2lem3  21908  ovolicc2lem4  21909  ovolicc2  21911  volsup  21944  dyadmbl  21987  vitalilem2  21996  vitalilem3  21997  mbfdm  22013  ismbf  22015  ismbf3d  22039  cncombf  22043  itg2seq  22127  itg2monolem2  22136  itg2monolem3  22137  itg2mono  22138  iblitg  22153  itgconst  22203  itgfsum  22211  limcvallem  22253  ellimc3  22261  cnlimci  22271  cnmptlimc  22272  dvferm1lem  22363  dvferm1  22364  dvferm2lem  22365  dvferm2  22366  dvlipcn  22373  dvle  22386  lhop1lem  22392  lhop1  22393  dvfsumge  22401  dvfsumlem2  22406  dvfsumlem3  22407  dvfsumlem4  22408  dvfsum2  22413  ftc1a  22416  ftc1lem4  22418  itgsubstlem  22427  fta1glem2  22545  fta1g  22546  plyeq0lem  22585  dgrcolem2  22649  dgrco  22650  plydivlem4  22670  plydivex  22671  fta1lem  22681  fta1  22682  vieta1lem2  22685  vieta1  22686  aalioulem2  22707  aalioulem4  22709  tayl0  22735  ulmi  22759  ulmclm  22760  ulmshftlem  22762  ulmcaulem  22767  ulmcau  22768  ulmcn  22772  ulmdvlem1  22773  ulmdvlem3  22775  ulmdv  22776  pserulm  22795  efif1olem4  22910  rlimcnp  23273  rlimcnp2  23274  xrlimcnp  23276  cxploglim  23285  scvxcvx  23293  wilthlem2  23321  ftalem3  23326  fsumdvdscom  23439  musumsum  23446  chtub  23465  fsumvma  23466  perfectlem2  23483  dchrelbas3  23491  dchrelbasd  23492  dchrn0  23503  dchrptlem2  23518  lgsval2lem  23559  lgsdirnn0  23592  lgsdinn0  23593  2sqlem6  23622  2sqlem10  23627  dchrisumlema  23651  dchrisumlem1  23652  dchrisumlem2  23653  dchrisumlem3  23654  dchrmusum2  23657  dchrvmasumlem2  23661  dchrvmasumlem3  23662  dchrvmasumiflem1  23664  dchrisum0flblem2  23672  dchrisum0flb  23673  dchrisum0lem1b  23678  dchrisum0lem2  23681  2vmadivsumlem  23703  chpdifbndlem1  23716  selberg3lem1  23720  selberg4lem1  23723  pntrsumbnd2  23730  pntrlog2bndlem2  23741  pntrlog2bndlem3  23742  pntrlog2bndlem5  23744  pntrlog2bndlem6  23746  pntpbnd1  23749  pntibndlem2  23754  pntibndlem3  23755  pntibnd  23756  pntlemn  23763  pntlemj  23766  pntlemi  23767  pntlemo  23770  pntlem3  23772  pntleml  23774  ostth2lem1  23781  ostth2lem2  23797  ostth3  23801  brbtwn2  24186  colinearalg  24191  axcontlem4  24248  nbgra0nb  24407  nbgrassovt  24413  cusgrarn  24437  usgrasscusgra  24461  wwlknredwwlkn  24704  wwlkextproplem2  24720  clwwlkf1  24774  clwwlkext2edg  24780  clwwisshclwwlem1  24783  clwlkf1clwwlklem  24827  nbhashnn0  24892  rusgraprop4  24922  3cyclfrgrarn1  24990  n4cyclfrgra  24996  frgrawopreglem4  25025  frgrawopreg1  25028  frgrawopreg2  25029  extwwlkfablem2  25056  isgrpo  25176  isgrp2d  25215  opidonOLD  25302  exidu1  25306  rngoideu  25364  blocnilem  25697  ip2eqi  25750  ubthlem1  25764  minvecolem3  25770  htthlem  25812  hial0  25997  hial02  25998  hial2eq  26001  ocorth  26187  occllem  26199  pjhthlem1  26287  h1de2i  26449  pjjsi  26596  lnopunilem1  26907  lnophmlem1  26913  nmcexi  26923  riesz4i  26960  mdi  27192  mdbr3  27194  mdbr4  27195  dmdi  27199  dmdbr3  27202  dmdbr4  27203  dmdi4  27204  mdslmd1i  27226  atss  27243  atom1d  27250  atmd  27296  sumdmdlem2  27316  cdj1i  27330  cdj3i  27338  nn0min  27589  archiabllem1a  27713  archiabllem2a  27716  archiabl  27720  isarchiofld  27785  crefi  27828  pcmplfin  27841  fmcncfil  27891  sigaclcu  28095  unelsiga  28112  measvun  28158  mbfmcnvima  28206  sibfima  28258  lgamgulmlem5  28553  lgambdd  28557  lgamcvglem  28560  derangenlem  28593  subfacp1lem5  28606  subfacp1lem6  28607  rescon  28669  cvmcov  28686  cvmliftlem3  28710  cvmlift2lem10  28735  cvmliftphtlem  28740  mclsax  28907  ghomgrpilem1  29003  ghomf1olem  29012  dfon2lem6  29196  poseq  29309  soseq  29310  nocvxminlem  29426  nobndlem6  29433  fin2so  30016  mbfresfi  30037  ftc1cnnclem  30064  opnrebl2  30115  nn0prpwlem  30116  nn0prpw  30117  neibastop2lem  30154  neibastop2  30155  filnetlem4  30175  seqpo  30216  incsequz  30217  mettrifi  30226  geomcau  30228  caushft  30230  sstotbnd2  30246  equivtotbnd  30250  totbndbnd  30261  ismtybndlem  30278  heibor1lem  30281  bfplem2  30295  isdrngo2  30337  unichnidl  30404  incssnn0  30619  lnmlssfg  31002  unxpwdom3  31017  fnchoice  31358  limcrecl  31589  fourierdlem54  31897  fourierdlem103  31946  fourierdlem104  31947  lcosslsp  32909  linindslinci  32919  lindslinindsimp1  32928  ldepsnlinclem1  32976  ldepsnlinclem2  32977  lsat0cv  34633  lcvexchlem4  34637  lcvexchlem5  34638  eqlkr3  34701  lub0N  34789  glb0N  34793  cvrnbtwn  34871  ltrneq2  35747  trlval2  35763  lpolsatN  37090  lpolpolsatN  37091  hdmap14lem12  37484
  Copyright terms: Public domain W3C validator