Theorem rspcv 3305

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

Step	Hyp	Ref	Expression
1		nfv 1843	. 2 |- F/ x ps
2		rspcv.1	. 2 |- ( x = A -> ( ph <-> ps ) )
3	1, 2	rspc 3303	1 |- ( A e. B -> ( A. x e. B ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202

This theorem is referenced by:  rspccv  3306  rspcva  3307  rspccva  3308  rspcda  3315  rspc3v  3325  rr19.3v  3345  rr19.28v  3346  rspsbc  3518  intmin  4497  ralxfrALT  4887  somo  5069  fr2nr  5092  nvocnv  6537  weniso  6604  knatar  6607  caofref  6923  fr3nr  6979  limuni3  7052  tfinds  7059  funcnvuni  7119  suppfnss  7320  onnseq  7441  smo11  7461  tfrlem1  7472  tfrlem5  7476  tfrlem9  7481  tz7.49  7540  omeulem1  7662  oeordi  7667  nneneq  8143  frfi  8205  unblem2  8213  unbnn2  8217  xpfi  8231  ordiso2  8420  ordtypelem6  8428  ordtypelem7  8429  cantnflem1c  8584  cantnflem1  8586  rankunb  8713  tcrank  8747  carduni  8807  dfac8alem  8852  acni  8868  alephinit  8918  aceq3lem  8943  dfac5  8951  dfac12lem2  8966  dfac12r  8968  dfac12k  8969  pwsdompw  9026  cflm  9072  fin2i  9117  isfin2-2  9141  fin23lem17  9160  fin23lem39  9172  isf32lem1  9175  isf32lem2  9176  isf34lem4  9199  hsmexlem4  9251  axcc3  9260  domtriomlem  9264  axdc3lem2  9273  axdc4lem  9277  axcclem  9279  ttukeylem5  9335  ttukeylem6  9336  axdclem  9341  alephval2  9394  canth4  9469  pwfseqlem5  9485  winainflem  9515  wununi  9528  wunpw  9529  eltskm  9665  dedekind  10200  squeeze0  10926  fiminre  10972  lbreu  10973  nnsub  11059  ublbneg  11773  zsupss  11777  uzwo3  11783  zmax  11785  zbtwnre  11786  xrub  12142  infmremnf  12173  infmrp1  12174  fzrevral  12425  axdc4uzlem  12782  seqcl2  12819  seqcl  12821  seqf  12822  seqfveq2  12823  seqfveq  12825  monoord  12831  monoord2  12832  sermono  12833  seqcaopr3  12836  seqid  12846  seqid2  12847  seqhomo  12848  seqz  12849  discr1  13000  discr  13001  faclbnd4lem4  13083  hashbclem  13236  ccatalpha  13375  wrdind  13476  wrd2ind  13477  reuccats1lem  13479  recan  14076  cau3lem  14094  caubnd2  14097  limsupgre  14212  climi  14241  rlimi  14244  rlimclim1  14276  rlimclim  14277  climrlim2  14278  climshftlem  14305  rlimcld2  14309  rlimcn1  14319  climcn1  14322  subcn2  14325  isercoll  14398  isercoll2  14399  climcau  14401  caucvgrlem  14403  caucvgb  14410  serf0  14411  iseraltlem2  14413  iseraltlem3  14414  iseralt  14415  fsumm1  14480  fsum1p  14482  fsumcom2  14505  fsumcom2OLD  14506  fsumge1  14529  telfsumo  14534  telfsumo2  14535  fsumparts  14538  o1fsum  14545  isum1p  14573  isumnn0nn  14574  isumrpcl  14575  climcndslem1  14581  climcndslem2  14582  climcnds  14583  cvgrat  14615  mertenslem1  14616  mertens  14618  clim2prod  14620  ntrivcvgfvn0  14631  fprodm1  14697  fprod1p  14698  fprodcom2  14714  fprodcom2OLD  14715  sqrt2irr  14979  ndvdssub  15133  dfgcd2  15263  lcmf  15346  lcmfunsnlem1  15350  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  lcmfdvds  15355  lcmfdvdsb  15356  lcmfunsn  15357  coprmgcdb  15362  coprmdvds1  15365  coprmprod  15375  coprmproddvdslem  15376  prmind2  15398  nprm  15401  dvdsprm  15415  coprm  15423  pcmpt  15596  pcmpt2  15597  pcmptdvds  15598  pcfac  15603  prmpwdvds  15608  unbenlem  15612  prmreclem4  15623  vdwlem1  15685  vdwlem2  15686  vdwlem9  15693  vdwlem10  15694  vdwlem13  15697  vdwnnlem1  15699  rami  15719  ramcl  15733  prmdvdsprmop  15747  prmodvdslcmf  15751  prmgaplcmlem1  15755  prmgaplem7  15761  catidex  16335  catideu  16336  iscatd2  16342  catlid  16344  catrid  16345  subcidcl  16504  funcid  16530  initoid  16655  termoid  16656  initoeu1  16661  termoeu1  16668  yonedalem4c  16917  yonffthlem  16922  isdrs2  16939  lublecllem  16988  lubun  17123  poslubmo  17146  posglbmo  17147  sgrp2rid2ex  17414  dfgrp2  17447  grpidd2  17459  grpidinv2  17474  dfgrp3lem  17513  mulgsubcl  17555  issubg4  17613  ghmf1  17689  fislw  18040  efgi  18132  efgi2  18138  efgsdmi  18145  efgsrel  18147  gexexlem  18255  gsummhm2  18339  dprdcntz  18407  dprddisj  18408  dprdss  18428  dprd2dlem2  18439  dprd2da  18441  dpjrid  18461  pgpfac1lem1  18473  pgpfaclem2  18481  srgrz  18526  srglz  18527  srgisid  18528  f1rhm0to0ALT  18741  issrngd  18861  islmodd  18869  rmodislmod  18931  islmhm2  19038  islbs2  19154  lbsextlem4  19161  rrgeq0i  19289  mvrf1  19425  mplsubglem  19434  mpllsslem  19435  subrgasclcl  19499  cply1mul  19664  prmirredlem  19841  ip2eq  19998  frlmphl  20120  mdetralt  20414  isclo2  20892  lmcvg  21066  cnpnei  21068  iscncl  21073  cncls  21078  lmss  21102  lmff  21105  cnt0  21150  isnrm2  21162  cnrmi  21164  isreg2  21181  tgcmp  21204  uncmp  21206  fiuncmp  21207  dfconn2  21222  1stcclb  21247  1stcfb  21248  2ndcctbss  21258  1stcelcls  21264  restnlly  21285  islly2  21287  lly1stc  21299  comppfsc  21335  kgeni  21340  kgencn2  21360  ptpjpre1  21374  ptbasfi  21384  ptpjopn  21415  dfac14  21421  txtube  21443  txlm  21451  cnmpt11  21466  cnmpt21  21474  cnmptkp  21483  cnmptk1p  21488  qtopomap  21521  qtopcmap  21522  kqfvima  21533  kqt0lem  21539  isr0  21540  nrmr0reg  21552  fgss2  21678  isufil2  21712  cfinufil  21732  flimopn  21779  fbflim2  21781  flimcf  21786  flfneii  21796  cnpflf  21805  fclssscls  21822  fclsnei  21823  fclsrest  21828  fclscf  21829  flimfnfcls  21832  fclscmp  21834  isfcf  21838  fcfnei  21839  alexsubALTlem3  21853  alexsubALTlem4  21854  alexsubALT  21855  ptcmplem3  21858  tgpt0  21922  tsmsi  21937  tsmsgsum  21942  tsmsres  21947  tsmsxplem1  21956  tsmsxplem2  21957  tsmsxp  21958  ustincl  22011  ustdiag  22012  ustinvel  22013  ustexhalf  22014  ucnima  22085  ucncn  22089  cfiluexsm  22094  psmet0  22113  imasdsf1olem  22178  prdsbl  22296  metss  22313  comet  22318  metcnp3  22345  isngp4  22416  nmoi  22532  mulc1cncf  22708  cncfco  22710  cnheiborlem  22753  cnheibor  22754  bndth  22757  lebnumii  22765  nmoleub2lem2  22916  nmoleub3  22919  ipcau2  23033  tchcphlem1  23034  tchcphlem2  23035  lmmcvg  23059  iscfil3  23071  iscau2  23075  iscau4  23077  cmetcaulem  23086  iscmet3lem1  23089  iscmet3lem2  23090  equivcfil  23097  equivcau  23098  lmcau  23111  pjthlem1  23208  pjthlem2  23209  ivthlem1  23220  ivthlem2  23221  ivthlem3  23222  ivth2  23224  ivthle  23225  ivthle2  23226  ivthicc  23227  ovoliunlem1  23270  ovolshftlem1  23277  ovolscalem1  23281  ovolicc2lem3  23287  ovolicc2lem4  23288  ovolicc2  23290  volsup  23324  dyadmbl  23368  vitalilem2  23378  vitalilem3  23379  mbfdm  23395  ismbf  23397  ismbf3d  23421  cncombf  23425  itg2seq  23509  itg2monolem2  23518  itg2monolem3  23519  itg2mono  23520  iblitg  23535  itgconst  23585  itgfsum  23593  limcvallem  23635  ellimc3  23643  cnlimci  23653  cnmptlimc  23654  dvferm1lem  23747  dvferm1  23748  dvferm2lem  23749  dvferm2  23750  dvlipcn  23757  dvle  23770  lhop1lem  23776  lhop1  23777  dvfsumge  23785  dvfsumlem2  23790  dvfsumlem3  23791  dvfsumlem4  23792  dvfsum2  23797  ftc1a  23800  ftc1lem4  23802  itgsubstlem  23811  fta1glem2  23926  fta1g  23927  plyeq0lem  23966  dgrcolem2  24030  dgrco  24031  plydivlem4  24051  plydivex  24052  fta1lem  24062  fta1  24063  vieta1lem2  24066  vieta1  24067  aalioulem2  24088  aalioulem4  24090  ulmi  24140  ulmclm  24141  ulmshftlem  24143  ulmcaulem  24148  ulmcau  24149  ulmcn  24153  ulmdvlem1  24154  ulmdvlem3  24156  ulmdv  24157  pserulm  24176  efif1olem4  24291  rlimcnp  24692  rlimcnp2  24693  xrlimcnp  24695  cxploglim  24704  scvxcvx  24712  lgamgulmlem5  24759  lgambdd  24763  wilthlem2  24795  ftalem3  24801  fsumdvdscom  24911  musumsum  24918  chtub  24937  fsumvma  24938  perfectlem2  24955  dchrelbas3  24963  dchrelbasd  24964  dchrn0  24975  dchrptlem2  24990  lgsval2lem  25032  lgsdirnn0  25069  lgsdinn0  25070  2sqlem6  25148  2sqlem10  25153  dchrisumlema  25177  dchrisumlem1  25178  dchrisumlem2  25179  dchrisumlem3  25180  dchrmusum2  25183  dchrvmasumlem2  25187  dchrvmasumlem3  25188  dchrvmasumiflem1  25190  dchrisum0flblem2  25198  dchrisum0flb  25199  dchrisum0lem1b  25204  dchrisum0lem2  25207  2vmadivsumlem  25229  chpdifbndlem1  25242  selberg3lem1  25246  selberg4lem1  25249  pntrsumbnd2  25256  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntpbnd1  25275  pntibndlem2  25280  pntibndlem3  25281  pntibnd  25282  pntlemn  25289  pntlemj  25292  pntlemi  25293  pntlemo  25296  pntlem3  25298  pntleml  25300  ostth2lem1  25307  ostth2lem2  25323  ostth3  25327  brbtwn2  25785  colinearalg  25790  axcontlem4  25847  usgruspgrb  26076  cusgredg  26320  cusgrres  26344  usgredgsscusgredg  26355  fusgrn0degnn0  26395  wlk1walk  26535  wlkres  26567  wlkp1lem6  26575  wlkdlem2  26580  upgrwlkdvdelem  26632  pthdlem2lem  26663  lfgrn1cycl  26697  wwlksnredwwlkn  26790  wwlksnextproplem2  26805  clwwlksf1  26917  clwwlksext2edg  26923  clwwisshclwwslemlem  26926  clwlksf1clwwlklem  26968  eupth2lem3  27096  rspc2vd  27129  3cyclfrgrrn1  27149  n4cyclfrgr  27155  frgrwopregasn  27180  frgrwopregbsn  27181  isgrpo  27351  blocnilem  27659  ip2eqi  27712  ubthlem1  27726  minvecolem3  27732  htthlem  27774  hial0  27959  hial02  27960  hial2eq  27963  ocorth  28150  occllem  28162  pjhthlem1  28250  h1de2i  28412  pjjsi  28559  lnopunilem1  28869  lnophmlem1  28875  nmcexi  28885  riesz4i  28922  mdi  29154  mdbr3  29156  mdbr4  29157  dmdi  29161  dmdbr3  29164  dmdbr4  29165  dmdi4  29166  mdslmd1i  29188  atss  29205  atom1d  29212  atmd  29258  sumdmdlem2  29278  cdj1i  29292  cdj3i  29300  nn0min  29567  archiabllem1a  29745  archiabllem2a  29748  archiabl  29752  isarchiofld  29817  crefi  29914  pcmplfin  29927  fmcncfil  29977  sigaclcu  30180  unelsiga  30197  sigapildsys  30225  ldgenpisys  30229  measvun  30272  mbfmcnvima  30319  carsgclctunlem2  30381  sibfima  30400  derangenlem  31153  subfacp1lem5  31166  subfacp1lem6  31167  resconn  31228  cvmcov  31245  cvmliftlem3  31269  cvmliftphtlem  31299  mclsax  31466  dfon2lem6  31693  poseq  31750  soseq  31751  nolt02o  31845  noresle  31846  noprefixmo  31848  nosupbnd1lem1  31854  nosupbnd1lem4  31857  nosupbnd2lem1  31861  nosupbnd2  31862  nocvxminlem  31893  fwddifnp1  32272  opnrebl2  32316  nn0prpwlem  32317  nn0prpw  32318  neibastop2lem  32355  neibastop2  32356  filnetlem4  32376  bj-mooreset  33056  bj-ismoored0  33061  bj-ismoored  33062  dfgcd3  33170  fin2so  33396  poimirlem25  33434  poimirlem29  33438  poimir  33442  mbfresfi  33456  ftc1cnnclem  33483  seqpo  33543  incsequz  33544  mettrifi  33553  geomcau  33555  caushft  33557  sstotbnd2  33573  equivtotbnd  33577  totbndbnd  33588  ismtybndlem  33605  heibor1lem  33608  bfplem2  33622  opidonOLD  33651  exidu1  33655  rngoideu  33702  isdrngo2  33757  unichnidl  33830  lsat0cv  34320  lcvexchlem4  34324  lcvexchlem5  34325  eqlkr3  34388  lub0N  34476  glb0N  34480  cvrnbtwn  34558  ltrneq2  35434  trlval2  35450  lpolsatN  36777  lpolpolsatN  36778  hdmap14lem12  37171  incssnn0  37274  lnmlssfg  37650  unxpwdom3  37665  neik0pk1imk0  38345  fnchoice  39188  limcrecl  39861  fourierdlem54  40377  fourierdlem103  40426  fourierdlem104  40427  smonoord  41341  iccpartlt  41360  iccpartgt  41363  iccpartdisj  41373  reuccatpfxs1lem  41433  fmtnodvds  41456  perfectALTVlem2  41631  sbgoldbwt  41665  sbgoldbst  41666  sgoldbeven3prm  41671  mogoldbb  41673  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  bgoldbnnsum3prm  41692  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbndlem4  41696  bgoldbtbnd  41697  tgblthelfgott  41703  tgoldbach  41705  tgblthelfgottOLD  41709  tgoldbachOLD  41712  lcosslsp  42227  linindslinci  42237  lindslinindsimp1  42246  ldepsnlinclem1  42294  ldepsnlinclem2  42295