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

Theorem rspcv 3131
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 1715 . 2  |-  F/ x ps
2 rspcv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2rspc 3129 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1399    e. wcel 1826   A.wral 2732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ral 2737  df-v 3036
This theorem is referenced by:  rspccv  3132  rspcva  3133  rspccva  3134  rspc3v  3147  rr19.3v  3166  rr19.28v  3167  rspsbc  3331  intmin  4219  ralxfrALT  4581  somo  4748  fr2nr  4771  nvocnv  6088  weniso  6151  knatar  6154  grprinvlem  6412  grprinvd  6413  caofref  6465  fr3nr  6514  limuni3  6586  tfinds  6593  funcnvuni  6652  suppfnss  6843  onnseq  6933  smo11  6953  tfrlem1  6963  tfrlem5  6967  tfrlem9  6972  tz7.49  7028  omeulem1  7149  oeordi  7154  nneneq  7619  frfi  7680  unblem2  7688  unbnn2  7692  xpfi  7706  ordiso2  7855  ordtypelem6  7863  ordtypelem7  7864  cantnflem1c  8019  cantnflem1  8021  cantnflem1cOLD  8042  cantnflem1OLD  8044  rankunb  8181  tcrank  8215  carduni  8275  dfac8alem  8323  acni  8339  alephinit  8389  aceq3lem  8414  dfac5  8422  dfac12lem2  8437  dfac12r  8439  dfac12k  8440  pwsdompw  8497  cflm  8543  fin1ai  8586  fin2i  8588  isfin2-2  8612  fin23lem17  8631  fin23lem39  8643  isf32lem1  8646  isf32lem2  8647  isf34lem4  8670  hsmexlem4  8722  axcc3  8731  domtriomlem  8735  axdc3lem2  8744  axdc4lem  8748  axcclem  8750  ttukeylem5  8806  ttukeylem6  8807  axdclem  8812  alephval2  8860  canth4  8936  pwfseqlem5  8952  winainflem  8982  wununi  8995  wunpw  8996  eltskm  9132  dedekind  9655  squeeze0  10364  lbreu  10409  nnsub  10491  ublbneg  11085  zsupss  11090  uzwo3  11096  zmax  11098  zbtwnre  11099  xrub  11424  fzrevral  11685  axdc4uzlem  11995  seqcl2  12028  seqcl  12030  seqf  12031  seqfveq2  12032  seqfveq  12034  seqshft2  12036  monoord  12040  monoord2  12041  sermono  12042  seqsplit  12043  seqcaopr3  12045  seqid  12055  seqid2  12056  seqhomo  12057  seqz  12058  discr1  12204  discr  12205  faclbnd4lem4  12276  hashbclem  12405  wrdind  12613  wrd2ind  12614  reuccats1lem  12616  recan  13171  cau3lem  13189  caubnd2  13192  limsupgre  13306  climi  13335  rlimi  13338  rlimclim1  13370  rlimclim  13371  climrlim2  13372  climshftlem  13399  rlimcld2  13403  rlimcn1  13413  climcn1  13416  subcn2  13419  isercoll  13492  isercoll2  13493  climcau  13495  caucvgrlem  13497  caucvgb  13504  serf0  13505  iseraltlem2  13507  iseraltlem3  13508  iseralt  13509  fsumm1  13568  fsum1p  13570  fsumcom2  13591  fsumge1  13613  telfsumo  13618  telfsumo2  13619  fsumparts  13622  o1fsum  13629  isum1p  13655  isumnn0nn  13656  isumrpcl  13657  climcndslem1  13663  climcndslem2  13664  climcnds  13665  cvgrat  13694  mertenslem1  13695  mertens  13697  clim2prod  13699  ntrivcvgfvn0  13710  fprodm1  13773  fprod1p  13774  fprodcom2  13790  sqrt2irr  13984  ndvdssub  14067  prmind2  14230  nprm  14233  dvdsprm  14242  coprm  14243  pcmpt  14413  pcmpt2  14414  pcmptdvds  14415  pcfac  14420  prmpwdvds  14424  unbenlem  14428  prmreclem4  14439  prmreclem5  14440  vdwlem1  14501  vdwlem2  14502  vdwlem9  14509  vdwlem10  14510  vdwlem13  14513  vdwnnlem1  14515  rami  14535  ramcl  14549  catidex  15081  catideu  15082  iscatd2  15088  catlid  15090  catrid  15091  subcidcl  15250  funcid  15276  initoid  15401  termoid  15402  initoeu1  15407  termoeu1  15414  yonedalem4c  15663  yonffthlem  15668  isdrs2  15685  lublecllem  15735  lubun  15870  poslubmo  15893  posglbmo  15894  sgrp2rid2ex  16162  grpidd2  16204  mulgsubcl  16273  issubg4  16337  ghmf1  16412  fislw  16762  efgi  16854  efgi2  16860  efgsdmi  16867  efgsrel  16869  gexexlem  16975  gsumzaddlem  17051  gsumzaddlemOLD  17053  gsummhm2  17077  gsummhm2OLD  17078  dprdcntz  17154  dprddisj  17155  dprdss  17189  dprd2dlem2  17202  dprd2da  17204  dpjrid  17224  ablfac1eu  17237  pgpfac1lem1  17238  pgpfaclem2  17246  srgrz  17290  srglz  17291  srgisid  17292  f1rhm0to0ALT  17503  issrngd  17623  islmodd  17631  islmhm2  17797  islbs2  17913  lbsextlem4  17920  rrgeq0i  18050  mvrf1  18194  mplsubglem  18206  mpllsslem  18207  mplsubglemOLD  18208  mpllsslemOLD  18209  subrgasclcl  18277  cply1mul  18448  prmirredlem  18623  ip2eq  18779  frlmphl  18901  mdetralt  19195  isclo2  19675  lmcvg  19849  cnpnei  19851  iscncl  19856  cncls  19861  lmss  19885  lmff  19888  cnt0  19933  isnrm2  19945  cnrmi  19947  isreg2  19964  cmpcov  19975  tgcmp  19987  uncmp  19989  fiuncmp  19990  dfcon2  20005  1stcclb  20030  1stcfb  20031  2ndcctbss  20041  1stcelcls  20047  restnlly  20068  islly2  20070  lly1stc  20082  comppfsc  20118  kgeni  20123  kgencn2  20143  ptpjpre1  20157  ptbasfi  20167  ptpjopn  20198  dfac14  20204  txtube  20226  txlm  20234  cnmpt11  20249  cnmpt21  20257  cnmptkp  20266  cnmptk1p  20271  qtopomap  20304  qtopcmap  20305  kqfvima  20316  kqt0lem  20322  isr0  20323  nrmr0reg  20335  fgss2  20460  isufil2  20494  cfinufil  20514  flimopn  20561  fbflim2  20563  flimcf  20568  flfneii  20578  cnpflf  20587  fclssscls  20604  fclsnei  20605  fclsrest  20610  fclscf  20611  flimfnfcls  20614  fclscmp  20616  isfcf  20620  fcfnei  20621  alexsubALTlem3  20634  alexsubALTlem4  20635  alexsubALT  20636  ptcmplem3  20639  tgpt0  20702  tsmsi  20717  tsmsgsum  20722  tsmsgsumOLD  20725  tsmsresOLD  20730  tsmsres  20731  tsmsxplem1  20740  tsmsxplem2  20741  tsmsxp  20742  ustincl  20795  ustdiag  20796  ustinvel  20797  ustexhalf  20798  ucnima  20869  ucncn  20873  cfiluexsm  20878  psmet0  20897  imasdsf1olem  20961  prdsbl  21079  metss  21096  comet  21101  metcnp3  21128  isngp4  21216  nmoi  21320  mulc1cncf  21494  cncfco  21496  cnheiborlem  21539  cnheibor  21540  bndth  21543  lebnumii  21551  nmoleub2lem2  21684  nmoleub3  21687  ipcau2  21762  tchcphlem1  21763  tchcphlem2  21764  lmmcvg  21785  iscfil3  21797  iscau2  21801  iscau4  21803  cmetcaulem  21812  iscmet3lem1  21815  iscmet3lem2  21816  equivcfil  21823  equivcau  21824  lmcau  21836  pjthlem1  21937  pjthlem2  21938  ivthlem1  21948  ivthlem2  21949  ivthlem3  21950  ivth2  21952  ivthle  21953  ivthle2  21954  ivthicc  21955  ovoliunlem1  21998  ovolshftlem1  22005  ovolscalem1  22009  ovolicc2lem3  22015  ovolicc2lem4  22016  ovolicc2  22018  volsup  22051  dyadmbl  22094  vitalilem2  22103  vitalilem3  22104  mbfdm  22120  ismbf  22122  ismbf3d  22146  cncombf  22150  itg2seq  22234  itg2monolem2  22243  itg2monolem3  22244  itg2mono  22245  iblitg  22260  itgconst  22310  itgfsum  22318  limcvallem  22360  ellimc3  22368  cnlimci  22378  cnmptlimc  22379  dvferm1lem  22470  dvferm1  22471  dvferm2lem  22472  dvferm2  22473  dvlipcn  22480  dvle  22493  lhop1lem  22499  lhop1  22500  dvfsumge  22508  dvfsumlem2  22513  dvfsumlem3  22514  dvfsumlem4  22515  dvfsum2  22520  ftc1a  22523  ftc1lem4  22525  itgsubstlem  22534  fta1glem2  22652  fta1g  22653  plyeq0lem  22692  dgrcolem2  22756  dgrco  22757  plydivlem4  22777  plydivex  22778  fta1lem  22788  fta1  22789  vieta1lem2  22792  vieta1  22793  aalioulem2  22814  aalioulem4  22816  tayl0  22842  ulmi  22866  ulmclm  22867  ulmshftlem  22869  ulmcaulem  22874  ulmcau  22875  ulmcn  22879  ulmdvlem1  22880  ulmdvlem3  22882  ulmdv  22883  pserulm  22902  efif1olem4  23017  rlimcnp  23412  rlimcnp2  23413  xrlimcnp  23415  cxploglim  23424  scvxcvx  23432  wilthlem2  23460  ftalem3  23465  fsumdvdscom  23578  musumsum  23585  chtub  23604  fsumvma  23605  perfectlem2  23622  dchrelbas3  23630  dchrelbasd  23631  dchrn0  23642  dchrptlem2  23657  lgsval2lem  23698  lgsdirnn0  23731  lgsdinn0  23732  2sqlem6  23761  2sqlem10  23766  dchrisumlema  23790  dchrisumlem1  23791  dchrisumlem2  23792  dchrisumlem3  23793  dchrmusum2  23796  dchrvmasumlem2  23800  dchrvmasumlem3  23801  dchrvmasumiflem1  23803  dchrisum0flblem2  23811  dchrisum0flb  23812  dchrisum0lem1b  23817  dchrisum0lem2  23820  2vmadivsumlem  23842  chpdifbndlem1  23855  selberg3lem1  23859  selberg4lem1  23862  pntrsumbnd2  23869  pntrlog2bndlem2  23880  pntrlog2bndlem3  23881  pntrlog2bndlem5  23883  pntrlog2bndlem6  23885  pntpbnd1  23888  pntibndlem2  23893  pntibndlem3  23894  pntibnd  23895  pntlemn  23902  pntlemj  23905  pntlemi  23906  pntlemo  23909  pntlem3  23911  pntleml  23913  ostth2lem1  23920  ostth2lem2  23936  ostth3  23940  brbtwn2  24329  colinearalg  24334  axcontlem4  24391  nbgra0nb  24550  nbgrassovt  24556  cusgrarn  24580  usgrasscusgra  24604  wwlknredwwlkn  24847  wwlkextproplem2  24863  clwwlkf1  24917  clwwlkext2edg  24923  clwwisshclwwlem1  24926  clwlkf1clwwlklem  24970  nbhashnn0  25035  rusgraprop4  25065  3cyclfrgrarn1  25133  n4cyclfrgra  25139  frgrawopreglem4  25168  frgrawopreg1  25171  frgrawopreg2  25172  extwwlkfablem2  25199  isgrpo  25315  isgrp2d  25354  opidonOLD  25441  exidu1  25445  rngoideu  25503  blocnilem  25836  ip2eqi  25889  ubthlem1  25903  minvecolem3  25909  htthlem  25951  hial0  26136  hial02  26137  hial2eq  26140  ocorth  26326  occllem  26338  pjhthlem1  26426  h1de2i  26588  pjjsi  26735  lnopunilem1  27045  lnophmlem1  27051  nmcexi  27061  riesz4i  27098  mdi  27330  mdbr3  27332  mdbr4  27333  dmdi  27337  dmdbr3  27340  dmdbr4  27341  dmdi4  27342  mdslmd1i  27364  atss  27381  atom1d  27388  atmd  27434  sumdmdlem2  27454  cdj1i  27468  cdj3i  27476  nn0min  27764  archiabllem1a  27888  archiabllem2a  27891  archiabl  27895  isarchiofld  27961  crefi  28004  pcmplfin  28017  fmcncfil  28067  sigaclcu  28266  unelsiga  28283  sigapildsys  28307  measvun  28336  mbfmcnvima  28384  carsgclctunlem2  28446  sibfima  28463  lgamgulmlem5  28764  lgambdd  28768  lgamcvglem  28771  derangenlem  28804  subfacp1lem5  28817  subfacp1lem6  28818  rescon  28880  cvmcov  28897  cvmliftlem3  28921  cvmlift2lem10  28946  cvmliftphtlem  28951  mclsax  29118  ghomgrpilem1  29214  ghomf1olem  29223  dfon2lem6  29385  poseq  29498  soseq  29499  nocvxminlem  29615  nobndlem6  29622  fin2so  30205  mbfresfi  30226  ftc1cnnclem  30254  opnrebl2  30305  nn0prpwlem  30306  nn0prpw  30307  neibastop2lem  30344  neibastop2  30345  filnetlem4  30365  seqpo  30406  incsequz  30407  mettrifi  30416  geomcau  30418  caushft  30420  sstotbnd2  30436  equivtotbnd  30440  totbndbnd  30451  ismtybndlem  30468  heibor1lem  30471  bfplem2  30485  isdrngo2  30527  unichnidl  30594  incssnn0  30809  lnmlssfg  31192  unxpwdom3  31207  fnchoice  31571  limcrecl  31801  fourierdlem54  32109  fourierdlem103  32158  fourierdlem104  32159  perfectALTVlem2  32544  reuccatpfxs1lem  32608  lcosslsp  33239  linindslinci  33249  lindslinindsimp1  33258  ldepsnlinclem1  33306  ldepsnlinclem2  33307  lsat0cv  35171  lcvexchlem4  35175  lcvexchlem5  35176  eqlkr3  35239  lub0N  35327  glb0N  35331  cvrnbtwn  35409  ltrneq2  36285  trlval2  36301  lpolsatN  37628  lpolpolsatN  37629  hdmap14lem12  38022
  Copyright terms: Public domain W3C validator