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

Theorem rspcv 3184
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 1754 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 3182 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 1870   A.wral 2782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-v 3089
This theorem is referenced by:  rspccv  3185  rspcva  3186  rspccva  3187  rspc3v  3200  rr19.3v  3219  rr19.28v  3220  rspsbc  3384  intmin  4278  ralxfrALT  4641  somo  4809  fr2nr  4832  nvocnv  6195  weniso  6260  knatar  6263  grprinvlem  6521  grprinvd  6522  caofref  6571  fr3nr  6620  limuni3  6693  tfinds  6700  funcnvuni  6760  suppfnss  6951  onnseq  7071  smo11  7091  tfrlem1  7102  tfrlem5  7106  tfrlem9  7111  tz7.49  7170  omeulem1  7291  oeordi  7296  nneneq  7761  frfi  7822  unblem2  7830  unbnn2  7834  xpfi  7848  ordiso2  8030  ordtypelem6  8038  ordtypelem7  8039  cantnflem1c  8191  cantnflem1  8193  rankunb  8320  tcrank  8354  carduni  8414  dfac8alem  8458  acni  8474  alephinit  8524  aceq3lem  8549  dfac5  8557  dfac12lem2  8572  dfac12r  8574  dfac12k  8575  pwsdompw  8632  cflm  8678  fin1ai  8721  fin2i  8723  isfin2-2  8747  fin23lem17  8766  fin23lem39  8778  isf32lem1  8781  isf32lem2  8782  isf34lem4  8805  hsmexlem4  8857  axcc3  8866  domtriomlem  8870  axdc3lem2  8879  axdc4lem  8883  axcclem  8885  ttukeylem5  8941  ttukeylem6  8942  axdclem  8947  alephval2  8995  canth4  9071  pwfseqlem5  9087  winainflem  9117  wununi  9130  wunpw  9131  eltskm  9267  dedekind  9796  squeeze0  10509  fiminre  10555  lbreu  10556  nnsub  10648  ublbneg  11248  zsupss  11253  uzwo3  11259  zmax  11261  zbtwnre  11262  xrub  11597  infmremnf  11633  infmrp1  11634  fzrevral  11877  axdc4uzlem  12192  seqcl2  12228  seqcl  12230  seqf  12231  seqfveq2  12232  seqfveq  12234  seqshft2  12236  monoord  12240  monoord2  12241  sermono  12242  seqsplit  12243  seqcaopr3  12245  seqid  12255  seqid2  12256  seqhomo  12257  seqz  12258  discr1  12405  discr  12406  faclbnd4lem4  12478  hashbclem  12610  wrdind  12818  wrd2ind  12819  reuccats1lem  12821  recan  13378  cau3lem  13396  caubnd2  13399  limsupgre  13520  limsupgreOLD  13521  climi  13552  rlimi  13555  rlimclim1  13587  rlimclim  13588  climrlim2  13589  climshftlem  13616  rlimcld2  13620  rlimcn1  13630  climcn1  13633  subcn2  13636  isercoll  13709  isercoll2  13710  climcau  13712  caucvgrlem  13714  caucvgrlemOLD  13715  caucvgb  13724  serf0  13725  iseraltlem2  13727  iseraltlem3  13728  iseralt  13729  fsumm1  13790  fsum1p  13792  fsumcom2  13813  fsumge1  13835  telfsumo  13840  telfsumo2  13841  fsumparts  13844  o1fsum  13851  isum1p  13877  isumnn0nn  13878  isumrpcl  13879  climcndslem1  13885  climcndslem2  13886  climcnds  13887  cvgrat  13917  mertenslem1  13918  mertens  13920  clim2prod  13922  ntrivcvgfvn0  13933  fprodm1  13999  fprod1p  14000  fprodcom2  14016  sqrt2irr  14279  ndvdssub  14363  lcmf  14568  lcmfunsnlem1  14572  lcmfunsnlem2lem1  14573  lcmfunsnlem2lem2  14574  lcmfdvds  14577  lcmfdvdsb  14578  lcmfunsn  14579  prmind2  14597  nprm  14600  dvdsprm  14609  coprmgcdb  14616  coprm  14619  coprmprod  14640  coprmproddvdslem  14641  pcmpt  14791  pcmpt2  14792  pcmptdvds  14793  pcfac  14798  prmpwdvds  14802  unbenlem  14806  prmreclem4  14817  prmreclem5  14818  vdwlem1  14885  vdwlem2  14886  vdwlem9  14893  vdwlem10  14894  vdwlem13  14897  vdwnnlem1  14899  rami  14926  ramcl  14941  prmdvdsprmop  14955  prmodvdslcmf  14959  prmgaplcmlem1  14963  prmgaplcmlem1OLD  14966  prmdvdsprmorpOLD  14970  prmordvdslcmfOLD  14973  prmordvdslcmsOLDOLD  14975  prmgaplem7  14981  catidex  15522  catideu  15523  iscatd2  15529  catlid  15531  catrid  15532  subcidcl  15691  funcid  15717  initoid  15842  termoid  15843  initoeu1  15848  termoeu1  15855  yonedalem4c  16104  yonffthlem  16109  isdrs2  16126  lublecllem  16176  lubun  16311  poslubmo  16334  posglbmo  16335  sgrp2rid2ex  16603  grpidd2  16645  mulgsubcl  16714  issubg4  16778  ghmf1  16853  fislw  17203  efgi  17295  efgi2  17301  efgsdmi  17308  efgsrel  17310  gexexlem  17416  gsumzaddlem  17480  gsummhm2  17498  dprdcntz  17566  dprddisj  17567  dprdss  17588  dprd2dlem2  17599  dprd2da  17601  dpjrid  17621  ablfac1eu  17632  pgpfac1lem1  17633  pgpfaclem2  17641  srgrz  17685  srglz  17686  srgisid  17687  f1rhm0to0ALT  17895  issrngd  18015  islmodd  18023  islmhm2  18187  islbs2  18303  lbsextlem4  18310  rrgeq0i  18439  mvrf1  18575  mplsubglem  18584  mpllsslem  18585  subrgasclcl  18648  cply1mul  18813  prmirredlem  18986  ip2eq  19142  frlmphl  19261  mdetralt  19555  isclo2  20026  lmcvg  20200  cnpnei  20202  iscncl  20207  cncls  20212  lmss  20236  lmff  20239  cnt0  20284  isnrm2  20296  cnrmi  20298  isreg2  20315  cmpcov  20326  tgcmp  20338  uncmp  20340  fiuncmp  20341  dfcon2  20356  1stcclb  20381  1stcfb  20382  2ndcctbss  20392  1stcelcls  20398  restnlly  20419  islly2  20421  lly1stc  20433  comppfsc  20469  kgeni  20474  kgencn2  20494  ptpjpre1  20508  ptbasfi  20518  ptpjopn  20549  dfac14  20555  txtube  20577  txlm  20585  cnmpt11  20600  cnmpt21  20608  cnmptkp  20617  cnmptk1p  20622  qtopomap  20655  qtopcmap  20656  kqfvima  20667  kqt0lem  20673  isr0  20674  nrmr0reg  20686  fgss2  20811  isufil2  20845  cfinufil  20865  flimopn  20912  fbflim2  20914  flimcf  20919  flfneii  20929  cnpflf  20938  fclssscls  20955  fclsnei  20956  fclsrest  20961  fclscf  20962  flimfnfcls  20965  fclscmp  20967  isfcf  20971  fcfnei  20972  alexsubALTlem3  20986  alexsubALTlem4  20987  alexsubALT  20988  ptcmplem3  20991  tgpt0  21055  tsmsi  21070  tsmsgsum  21075  tsmsres  21080  tsmsxplem1  21089  tsmsxplem2  21090  tsmsxp  21091  ustincl  21144  ustdiag  21145  ustinvel  21146  ustexhalf  21147  ucnima  21218  ucncn  21222  cfiluexsm  21227  psmet0  21246  imasdsf1olem  21310  prdsbl  21428  metss  21445  comet  21450  metcnp3  21477  isngp4  21547  nmoi  21651  mulc1cncf  21824  cncfco  21826  cnheiborlem  21869  cnheibor  21870  bndth  21873  lebnumii  21881  nmoleub2lem2  22014  nmoleub3  22017  ipcau2  22092  tchcphlem1  22093  tchcphlem2  22094  lmmcvg  22115  iscfil3  22127  iscau2  22131  iscau4  22133  cmetcaulem  22142  iscmet3lem1  22145  iscmet3lem2  22146  equivcfil  22153  equivcau  22154  lmcau  22166  pjthlem1  22263  pjthlem2  22264  ivthlem1  22274  ivthlem2  22275  ivthlem3  22276  ivth2  22278  ivthle  22279  ivthle2  22280  ivthicc  22281  ovoliunlem1  22324  ovolshftlem1  22331  ovolscalem1  22335  ovolicc2lem3  22341  ovolicc2lem4  22342  ovolicc2  22344  volsup  22377  dyadmbl  22426  vitalilem2  22435  vitalilem3  22436  mbfdm  22452  ismbf  22454  ismbf3d  22478  cncombf  22482  itg2seq  22568  itg2monolem2  22577  itg2monolem3  22578  itg2mono  22579  iblitg  22594  itgconst  22644  itgfsum  22652  limcvallem  22694  ellimc3  22702  cnlimci  22712  cnmptlimc  22713  dvferm1lem  22804  dvferm1  22805  dvferm2lem  22806  dvferm2  22807  dvlipcn  22814  dvle  22827  lhop1lem  22833  lhop1  22834  dvfsumge  22842  dvfsumlem2  22847  dvfsumlem3  22848  dvfsumlem4  22849  dvfsum2  22854  ftc1a  22857  ftc1lem4  22859  itgsubstlem  22868  fta1glem2  22983  fta1g  22984  plyeq0lem  23023  dgrcolem2  23087  dgrco  23088  plydivlem4  23108  plydivex  23109  fta1lem  23119  fta1  23120  vieta1lem2  23123  vieta1  23124  aalioulem2  23145  aalioulem4  23147  tayl0  23173  ulmi  23197  ulmclm  23198  ulmshftlem  23200  ulmcaulem  23205  ulmcau  23206  ulmcn  23210  ulmdvlem1  23211  ulmdvlem3  23213  ulmdv  23214  pserulm  23233  efif1olem4  23350  rlimcnp  23747  rlimcnp2  23748  xrlimcnp  23750  cxploglim  23759  scvxcvx  23767  lgamgulmlem5  23814  lgambdd  23818  lgamcvglem  23821  wilthlem2  23850  ftalem3  23855  fsumdvdscom  23968  musumsum  23975  chtub  23994  fsumvma  23995  perfectlem2  24012  dchrelbas3  24020  dchrelbasd  24021  dchrn0  24032  dchrptlem2  24047  lgsval2lem  24088  lgsdirnn0  24121  lgsdinn0  24122  2sqlem6  24151  2sqlem10  24156  dchrisumlema  24180  dchrisumlem1  24181  dchrisumlem2  24182  dchrisumlem3  24183  dchrmusum2  24186  dchrvmasumlem2  24190  dchrvmasumlem3  24191  dchrvmasumiflem1  24193  dchrisum0flblem2  24201  dchrisum0flb  24202  dchrisum0lem1b  24207  dchrisum0lem2  24210  2vmadivsumlem  24232  chpdifbndlem1  24245  selberg3lem1  24249  selberg4lem1  24252  pntrsumbnd2  24259  pntrlog2bndlem2  24270  pntrlog2bndlem3  24271  pntrlog2bndlem5  24273  pntrlog2bndlem6  24275  pntpbnd1  24278  pntibndlem2  24283  pntibndlem3  24284  pntibnd  24285  pntlemn  24292  pntlemj  24295  pntlemi  24296  pntlemo  24299  pntlem3  24301  pntleml  24303  ostth2lem1  24310  ostth2lem2  24326  ostth3  24330  brbtwn2  24772  colinearalg  24777  axcontlem4  24834  nbgra0nb  24993  nbgrassovt  24999  cusgrarn  25023  usgrasscusgra  25047  wwlknredwwlkn  25290  wwlkextproplem2  25306  clwwlkf1  25360  clwwlkext2edg  25366  clwwisshclwwlem1  25369  clwlkf1clwwlklem  25413  nbhashnn0  25478  rusgraprop4  25508  3cyclfrgrarn1  25576  n4cyclfrgra  25582  frgrawopreglem4  25611  frgrawopreg1  25614  frgrawopreg2  25615  extwwlkfablem2  25642  isgrpo  25760  isgrp2d  25799  opidonOLD  25886  exidu1  25890  rngoideu  25948  blocnilem  26281  ip2eqi  26334  ubthlem1  26348  minvecolem3  26354  htthlem  26396  hial0  26581  hial02  26582  hial2eq  26585  ocorth  26770  occllem  26782  pjhthlem1  26870  h1de2i  27032  pjjsi  27179  lnopunilem1  27489  lnophmlem1  27495  nmcexi  27505  riesz4i  27542  mdi  27774  mdbr3  27776  mdbr4  27777  dmdi  27781  dmdbr3  27784  dmdbr4  27785  dmdi4  27786  mdslmd1i  27808  atss  27825  atom1d  27832  atmd  27878  sumdmdlem2  27898  cdj1i  27912  cdj3i  27920  nn0min  28213  archiabllem1a  28337  archiabllem2a  28340  archiabl  28344  isarchiofld  28410  crefi  28504  pcmplfin  28517  fmcncfil  28567  sigaclcu  28769  unelsiga  28786  sigapildsys  28814  ldgenpisys  28818  measvun  28861  mbfmcnvima  28909  carsgclctunlem2  28971  sibfima  28990  derangenlem  29673  subfacp1lem5  29686  subfacp1lem6  29687  rescon  29748  cvmcov  29765  cvmliftlem3  29789  cvmlift2lem10  29814  cvmliftphtlem  29819  mclsax  29986  ghomgrpilem1  30082  ghomf1olem  30091  dfon2lem6  30212  poseq  30269  soseq  30270  nocvxminlem  30355  nobndlem6  30362  fwddifnp1  30708  opnrebl2  30753  nn0prpwlem  30754  nn0prpw  30755  neibastop2lem  30792  neibastop2  30793  filnetlem4  30813  fin2so  31626  poimirlem25  31659  poimirlem29  31663  poimir  31667  mbfresfi  31681  ftc1cnnclem  31709  seqpo  31770  incsequz  31771  mettrifi  31780  geomcau  31782  caushft  31784  sstotbnd2  31800  equivtotbnd  31804  totbndbnd  31815  ismtybndlem  31832  heibor1lem  31835  bfplem2  31849  isdrngo2  31891  unichnidl  31958  lsat0cv  32298  lcvexchlem4  32302  lcvexchlem5  32303  eqlkr3  32366  lub0N  32454  glb0N  32458  cvrnbtwn  32536  ltrneq2  33412  trlval2  33428  lpolsatN  34755  lpolpolsatN  34756  hdmap14lem12  35149  incssnn0  35252  lnmlssfg  35634  unxpwdom3  35649  fnchoice  36980  limcrecl  37271  fourierdlem54  37582  fourierdlem103  37631  fourierdlem104  37632  smonoord  38098  iccpartlt  38118  iccpartgt  38121  iccpartdisj  38131  perfectALTVlem2  38224  bgoldbwt  38258  bgoldbst  38259  nnsum4primesodd  38271  nnsum4primesoddALTV  38272  bgoldbnnsum3prm  38279  bgoldbtbndlem2  38281  bgoldbtbndlem3  38282  bgoldbtbndlem4  38283  bgoldbtbnd  38284  tgblthelfgott  38288  tgoldbach  38291  reuccatpfxs1lem  38354  lcosslsp  38981  linindslinci  38991  lindslinindsimp1  39000  ldepsnlinclem1  39048  ldepsnlinclem2  39049
  Copyright terms: Public domain W3C validator