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

Theorem rspcv 3210
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 1683 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 3208 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-v 3115
This theorem is referenced by:  rspccv  3211  rspcva  3212  rspccva  3213  rspc3v  3226  rr19.3v  3245  rr19.28v  3246  rspsbc  3421  intmin  4302  ralxfrALT  4666  somo  4834  fr2nr  4857  nvocnv  6173  weniso  6236  knatar  6239  grprinvlem  6495  grprinvd  6496  caofref  6548  fr3nr  6593  limuni3  6665  tfinds  6672  funcnvuni  6734  onnseq  7012  smo11  7032  tfrlem1  7042  tfrlem5  7046  tfrlem9  7051  tz7.49  7107  omeulem1  7228  oeordi  7233  nneneq  7697  frfi  7761  unblem2  7769  unbnn2  7773  xpfi  7787  ordiso2  7936  ordtypelem6  7944  ordtypelem7  7945  cantnflem1c  8102  cantnflem1  8104  cantnflem1cOLD  8125  cantnflem1OLD  8127  rankunb  8264  tcrank  8298  carduni  8358  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  9021  pwfseqlem5  9037  winainflem  9067  wununi  9080  wunpw  9081  eltskm  9217  dedekind  9739  squeeze0  10444  lbreu  10489  nnsub  10570  ublbneg  11162  zsupss  11167  uzwo3  11173  zmax  11175  zbtwnre  11176  xrub  11499  fzrevral  11758  axdc4uzlem  12055  seqcl2  12088  seqcl  12090  seqf  12091  seqfveq2  12092  seqfveq  12094  seqshft2  12096  monoord  12100  monoord2  12101  sermono  12102  seqsplit  12103  seqcaopr3  12105  seqid  12115  seqid2  12116  seqhomo  12117  seqz  12118  discr1  12264  discr  12265  faclbnd4lem4  12336  hashbclem  12461  wrdind  12659  wrd2ind  12660  reuccats1lem  12662  recan  13125  cau3lem  13143  caubnd2  13146  limsupgre  13260  climi  13289  rlimi  13292  rlimclim1  13324  rlimclim  13325  climrlim2  13326  climshftlem  13353  rlimcld2  13357  rlimcn1  13367  climcn1  13370  subcn2  13373  isercoll  13446  isercoll2  13447  climcau  13449  caucvgrlem  13451  caucvgb  13458  serf0  13459  iseraltlem2  13461  iseraltlem3  13462  iseralt  13463  fsumm1  13522  fsum1p  13524  fsumcom2  13545  fsumge1  13567  telfsumo  13572  telfsumo2  13573  fsumparts  13576  o1fsum  13583  isum1p  13609  isumnn0nn  13610  isumrpcl  13611  climcndslem1  13617  climcndslem2  13618  climcnds  13619  cvgrat  13648  mertenslem1  13649  mertens  13651  sqrt2irr  13836  ndvdssub  13917  prmind2  14080  nprm  14083  dvdsprm  14092  coprm  14093  pcmpt  14263  pcmpt2  14264  pcmptdvds  14265  pcfac  14270  prmpwdvds  14274  unbenlem  14278  prmreclem4  14289  prmreclem5  14290  vdwlem1  14351  vdwlem2  14352  vdwlem9  14359  vdwlem10  14360  vdwlem13  14363  vdwnnlem1  14365  rami  14385  ramcl  14399  catidex  14922  catideu  14923  iscatd2  14929  catlid  14931  catrid  14932  subcidcl  15064  funcid  15090  yonedalem4c  15397  yonffthlem  15402  isdrs2  15419  lublecllem  15468  lubun  15603  poslubmo  15626  posglbmo  15627  grpidd2  15885  mulgsubcl  15953  issubg4  16012  ghmf1  16087  fislw  16438  efgi  16530  efgi2  16536  efgsdmi  16543  efgsrel  16545  gexexlem  16648  gsumzaddlem  16722  gsumzaddlemOLD  16724  gsummhm2  16749  gsummhm2OLD  16750  dprdcntz  16829  dprddisj  16830  dprdss  16863  dprd2dlem2  16876  dprd2da  16878  dpjrid  16898  ablfac1eu  16911  pgpfac1lem1  16912  pgpfaclem2  16920  srgrz  16964  srglz  16965  srgisid  16966  f1rhm0to0ALT  17170  issrngd  17290  islmodd  17298  islmhm2  17464  islbs2  17580  lbsextlem4  17587  rrgeq0i  17705  mvrf1  17849  mplsubglem  17861  mpllsslem  17862  mplsubglemOLD  17863  mpllsslemOLD  17864  subrgasclcl  17932  prmirredlem  18287  prmirredlemOLD  18290  ip2eq  18452  frlmphl  18576  mdetralt  18874  isclo2  19352  lmcvg  19526  cnpnei  19528  iscncl  19533  cncls  19538  lmss  19562  lmff  19565  cnt0  19610  isnrm2  19622  cnrmi  19624  isreg2  19641  cmpcov  19652  tgcmp  19664  uncmp  19666  fiuncmp  19667  bwthOLD  19674  dfcon2  19683  1stcclb  19708  1stcfb  19709  2ndcctbss  19719  1stcelcls  19725  restnlly  19746  islly2  19748  lly1stc  19760  kgeni  19770  kgencn2  19790  ptpjpre1  19804  ptbasfi  19814  ptpjopn  19845  dfac14  19851  txtube  19873  txlm  19881  cnmpt11  19896  cnmpt21  19904  cnmptkp  19913  cnmptk1p  19918  qtopomap  19951  qtopcmap  19952  kqfvima  19963  kqt0lem  19969  isr0  19970  nrmr0reg  19982  fgss2  20107  isufil2  20141  cfinufil  20161  flimopn  20208  fbflim2  20210  flimcf  20215  flfneii  20225  cnpflf  20234  fclssscls  20251  fclsnei  20252  fclsrest  20257  fclscf  20258  flimfnfcls  20261  fclscmp  20263  isfcf  20267  fcfnei  20268  alexsubALTlem3  20281  alexsubALTlem4  20282  alexsubALT  20283  ptcmplem3  20286  tgpt0  20349  tsmsi  20364  tsmsgsum  20369  tsmsgsumOLD  20372  tsmsresOLD  20377  tsmsres  20378  tsmsxplem1  20387  tsmsxplem2  20388  tsmsxp  20389  ustincl  20442  ustdiag  20443  ustinvel  20444  ustexhalf  20445  isucn2  20514  ucnima  20516  ucncn  20520  cfiluexsm  20525  psmet0  20544  imasdsf1olem  20608  prdsbl  20726  metss  20743  comet  20748  metcnp3  20775  isngp4  20863  nmoi  20967  mulc1cncf  21141  cncfco  21143  cnheiborlem  21186  cnheibor  21187  bndth  21190  lebnumii  21198  nmoleub2lem2  21331  nmoleub3  21334  ipcau2  21409  tchcphlem1  21410  tchcphlem2  21411  lmmcvg  21432  iscfil3  21444  iscau2  21448  iscau4  21450  cmetcaulem  21459  iscmet3lem1  21462  iscmet3lem2  21463  equivcfil  21470  equivcau  21471  lmcau  21483  pjthlem1  21584  pjthlem2  21585  ivthlem1  21595  ivthlem2  21596  ivthlem3  21597  ivth2  21599  ivthle  21600  ivthle2  21601  ivthicc  21602  ovoliunlem1  21645  ovolshftlem1  21652  ovolscalem1  21656  ovolicc2lem3  21662  ovolicc2lem4  21663  ovolicc2  21665  volsup  21698  dyadmbl  21741  vitalilem2  21750  vitalilem3  21751  mbfdm  21767  ismbf  21769  ismbf3d  21793  cncombf  21797  itg2seq  21881  itg2monolem2  21890  itg2monolem3  21891  itg2mono  21892  iblitg  21907  itgconst  21957  itgfsum  21965  limcvallem  22007  ellimc3  22015  cnlimci  22025  cnmptlimc  22026  dvferm1lem  22117  dvferm1  22118  dvferm2lem  22119  dvferm2  22120  dvlipcn  22127  dvle  22140  lhop1lem  22146  lhop1  22147  dvfsumge  22155  dvfsumlem2  22160  dvfsumlem3  22161  dvfsumlem4  22162  dvfsum2  22167  ftc1a  22170  ftc1lem4  22172  itgsubstlem  22181  fta1glem2  22299  fta1g  22300  plyeq0lem  22339  dgrcolem2  22402  dgrco  22403  plydivlem4  22423  plydivex  22424  fta1lem  22434  fta1  22435  vieta1lem2  22438  vieta1  22439  aalioulem2  22460  aalioulem4  22462  tayl0  22488  ulmi  22512  ulmclm  22513  ulmshftlem  22515  ulmcaulem  22520  ulmcau  22521  ulmcn  22525  ulmdvlem1  22526  ulmdvlem3  22528  ulmdv  22529  pserulm  22548  efif1olem4  22662  rlimcnp  23020  rlimcnp2  23021  xrlimcnp  23023  cxploglim  23032  scvxcvx  23040  wilthlem2  23068  ftalem3  23073  fsumdvdscom  23186  musumsum  23193  chtub  23212  fsumvma  23213  perfectlem2  23230  dchrelbas3  23238  dchrelbasd  23239  dchrn0  23250  dchrptlem2  23265  lgsval2lem  23306  lgsdirnn0  23339  lgsdinn0  23340  2sqlem6  23369  2sqlem10  23374  dchrisumlema  23398  dchrisumlem1  23399  dchrisumlem2  23400  dchrisumlem3  23401  dchrmusum2  23404  dchrvmasumlem2  23408  dchrvmasumlem3  23409  dchrvmasumiflem1  23411  dchrisum0flblem2  23419  dchrisum0flb  23420  dchrisum0lem1b  23425  dchrisum0lem2  23428  2vmadivsumlem  23450  chpdifbndlem1  23463  selberg3lem1  23467  selberg4lem1  23470  pntrsumbnd2  23477  pntrlog2bndlem2  23488  pntrlog2bndlem3  23489  pntrlog2bndlem5  23491  pntrlog2bndlem6  23493  pntpbnd1  23496  pntibndlem2  23501  pntibndlem3  23502  pntibnd  23503  pntlemn  23510  pntlemj  23513  pntlemi  23514  pntlemo  23517  pntlem3  23519  pntleml  23521  ostth2lem1  23528  ostth2lem2  23544  ostth3  23548  brbtwn2  23881  colinearalg  23886  axcontlem4  23943  nbgra0nb  24102  nbgrassovt  24108  cusgrarn  24132  usgrasscusgra  24156  wwlknredwwlkn  24399  wwlkextproplem2  24415  clwwlkf1  24469  clwwlkext2edg  24475  3cyclfrgrarn1  24685  n4cyclfrgra  24691  frgrawopreglem4  24721  frgrawopreg1  24724  frgrawopreg2  24725  extwwlkfablem2  24752  isgrpo  24871  isgrp2d  24910  opidon  24997  exidu1  25001  rngoideu  25059  blocnilem  25392  ip2eqi  25445  ubthlem1  25459  minvecolem3  25465  htthlem  25507  hial0  25692  hial02  25693  hial2eq  25696  ocorth  25882  occllem  25894  pjhthlem1  25982  h1de2i  26144  pjjsi  26291  lnopunilem1  26602  lnophmlem1  26608  nmcexi  26618  riesz4i  26655  mdi  26887  mdbr3  26889  mdbr4  26890  dmdi  26894  dmdbr3  26897  dmdbr4  26898  dmdi4  26899  mdslmd1i  26921  atss  26938  atom1d  26945  atmd  26991  sumdmdlem2  27011  cdj1i  27025  cdj3i  27033  nn0min  27276  archiabllem1a  27394  archiabllem2a  27397  archiabl  27401  rngurd  27438  isarchiofld  27467  fmcncfil  27546  sigaclcu  27754  unelsiga  27771  measvun  27817  mbfmcnvima  27865  sibfima  27917  signstfvneq0  28166  lgamgulmlem5  28212  lgambdd  28216  lgamcvglem  28219  derangenlem  28252  subfacp1lem5  28265  subfacp1lem6  28266  rescon  28328  cvmcov  28345  cvmliftlem3  28369  cvmlift2lem10  28394  cvmliftphtlem  28399  ghomgrpilem1  28497  ghomf1olem  28506  clim2prod  28596  ntrivcvgfvn0  28607  fprodm1  28670  fprod1p  28671  fprodcom2  28688  dfon2lem6  28794  poseq  28907  soseq  28908  nocvxminlem  29024  nobndlem6  29031  fin2so  29614  mbfresfi  29636  ftc1cnnclem  29663  opnrebl2  29714  nn0prpwlem  29715  nn0prpw  29716  comppfsc  29777  neibastop2lem  29779  neibastop2  29780  filnetlem4  29800  seqpo  29841  incsequz  29842  mettrifi  29851  geomcau  29853  caushft  29855  sstotbnd2  29871  equivtotbnd  29875  totbndbnd  29886  ismtybndlem  29903  heibor1lem  29906  bfplem2  29920  isdrngo2  29962  unichnidl  30029  incssnn0  30245  lnmlssfg  30630  unxpwdom3  30645  fnchoice  30982  fourierdlem54  31461  fourierdlem103  31510  fourierdlem104  31511  lcosslsp  32112  linindslinci  32122  lindslinindsimp1  32131  ldepsnlinclem1  32187  ldepsnlinclem2  32188  lsat0cv  33830  lcvexchlem4  33834  lcvexchlem5  33835  eqlkr3  33898  lub0N  33986  glb0N  33990  cvrnbtwn  34068  ltrneq2  34944  trlval2  34959  lpolsatN  36285  lpolpolsatN  36286  hdmap14lem12  36679
  Copyright terms: Public domain W3C validator