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

Theorem raleqbidv 2973
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)
Hypotheses
Ref Expression
raleqbidv.1  |-  ( ph  ->  A  =  B )
raleqbidv.2  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
raleqbidv  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Distinct variable groups:    x, A    x, B    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem raleqbidv
StepHypRef Expression
1 raleqbidv.1 . . 3  |-  ( ph  ->  A  =  B )
21raleqdv 2965 . 2  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43ralbidv 2799 . 2  |-  ( ph  ->  ( A. x  e.  B  ps  <->  A. x  e.  B  ch )
)
52, 4bitrd 256 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   A.wral 2709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ral 2714
This theorem is referenced by:  f12dfv  6126  f13dfv  6127  knatar  6202  ofrfval  6492  fmpt2x  6812  ovmptss  6827  marypha1lem  7895  supeq123d  7912  oieq1  7975  acneq  8420  isfin1a  8668  fpwwe2cbv  9001  fpwwe2lem2  9003  fpwwecbv  9015  fpwwelem  9016  eltskg  9121  elgrug  9163  cau3lem  13356  rlim  13497  ello1  13517  elo1  13528  caurcvg2  13682  caucvgb  13684  fsum2dlem  13769  fsumcom2  13773  fprod2dlem  13972  fprodcom2  13976  pcfac  14782  vdwpc  14868  rami  14910  prmgaplem7  14965  prdsval  15291  ismre  15434  isacs2  15497  acsfiel  15498  iscat  15516  iscatd  15517  catidex  15518  catideu  15519  cidfval  15520  cidval  15521  catlid  15527  catrid  15528  comfeq  15549  catpropd  15552  monfval  15575  issubc  15678  fullsubc  15693  isfunc  15707  funcpropd  15743  isfull  15753  isfth  15757  fthpropd  15764  natfval  15789  initoval  15830  termoval  15831  isposd  16139  lubfval  16162  glbfval  16175  ismgm  16427  grpidval  16441  gsumvalx  16451  gsumpropd  16453  gsumress  16457  issgrp  16466  ismnddef  16476  ismndOLD  16480  ismndd  16497  mndpropd  16500  ismhm  16522  resmhm  16544  isgrp  16615  grppropd  16622  isgrpd2e  16626  isnsg  16784  nmznsg  16799  isghm  16821  isga  16883  subgga  16892  gsmsymgrfix  17007  gsmsymgreq  17011  gexval  17165  gexvalOLD  17167  ispgp  17182  isslw  17198  sylow2blem2  17211  efgval  17305  efgi  17307  efgsdm  17318  cmnpropd  17377  iscmnd  17380  submcmn2  17417  gsumzaddlem  17492  dmdprd  17568  dprdcntz  17578  issrg  17679  isring  17722  ringpropd  17750  isirred  17865  abvfval  17984  abvpropd  18008  islmod  18033  islmodd  18035  lmodprop2d  18088  lssset  18095  islmhm  18188  reslmhm  18213  lmhmpropd  18234  islbs  18237  rrgval  18449  isdomn  18456  isassa  18477  isassad  18485  assapropd  18489  ltbval  18633  opsrval  18636  psgndiflemA  19106  isphl  19132  islindf  19307  islindf2  19309  lsslindf  19325  dmatval  19454  dmatcrng  19464  scmatcrng  19483  cpmat  19670  istopg  19862  restbas  20111  ordtrest2  20157  cnfval  20186  cnpfval  20187  ist0  20273  ishaus  20275  iscnrm  20276  isnrm  20288  ist0-2  20297  ishaus2  20304  nrmsep3  20308  iscmp  20340  is1stc  20393  isptfin  20468  islocfin  20469  kgenval  20487  kgencn2  20509  txbas  20519  ptval  20522  dfac14  20570  isfil  20799  isufil  20855  isufl  20865  flfcntr  20995  ucnval  21229  iscusp  21251  prdsxmslem2  21481  isnlm  21615  nmofval  21656  nmofvalOLD  21675  lebnumii  21934  iscau4  22186  iscmet  22191  iscmet3lem1  22198  iscmet3  22200  equivcmet  22222  ulmcaulem  23286  ulmcau  23287  fsumdvdscom  24051  dchrisumlem3  24266  pntibndlem2  24366  pntibnd  24368  pntlemp  24385  ostth2lem2  24409  trgcgrg  24497  tgcgr4  24513  isismt  24516  iscusgra  25121  cusgrarn  25124  cusgra1v  25126  cusgra2v  25127  cusgra3v  25129  usgrasscusgra  25148  isuvtx  25153  uvtxel  25154  cusgrauvtxb  25161  iswlk  25185  wlkelwrd  25195  istrl  25204  constr3trllem2  25316  isconngra  25337  isconngra1  25338  iswwlk  25348  wlkiswwlk2  25362  isclwwlk  25433  clwwlkprop  25435  clwlkisclwwlklem2  25451  isrgra  25591  isfrgra  25655  frgraunss  25660  frgra1v  25663  frgra2v  25664  frgra3v  25667  1vwmgra  25668  3vfriswmgra  25670  3cyclfrgrarn1  25677  n4cyclfrgra  25683  frgrancvvdeqlem4  25698  frgrawopreglem4  25712  frgrawopreg2  25716  frgraregorufr0  25717  isplig  25846  gidval  25878  isgrp2d  25900  isgrpda  25962  isass  25981  isexid  25982  elghomlem1OLD  26026  isrngo  26043  isrngod  26044  iscom2  26077  vci  26104  isvclem  26133  isnvlem  26166  lnoval  26330  ajfval  26387  isphg  26395  minvecolem3  26455  minvecolem3OLD  26465  htth  26508  ressprs  28362  isslmd  28464  resv1r  28547  iscref  28618  ordtrest2NEW  28676  fmcncfil  28684  issiga  28880  isrnsigaOLD  28881  isrnsiga  28882  isldsys  28925  ismeas  28968  carsgval  29082  issibf  29113  sitgfval  29121  signstfvneq0  29408  istrkg2d  29430  ispcon  29893  isscon  29896  txpcon  29902  cvxpcon  29912  cvmscbv  29928  iscvm  29929  cvmsdisj  29940  cvmsss2  29944  snmlval  30001  elmrsubrn  30105  ismfs  30134  mclsval  30148  fwddifnval  30874  poimirlem28  31875  cover2g  31948  seqpo  31983  incsequz2  31985  caushft  31997  ismtyval  32039  rngohomval  32110  idlval  32153  pridlval  32173  maxidlval  32179  lflset  32537  islfld  32540  isopos  32658  isoml  32716  isatl  32777  iscvlat  32801  ishlat1  32830  psubspset  33221  lautset  33559  pautsetN  33575  ldilfset  33585  ltrnfset  33594  dilfsetN  33630  trnfsetN  33633  trnsetN  33634  trlfset  33638  tendofset  34237  tendoset  34238  dihffval  34710  lpolsetN  34962  hdmapfval  35310  hgmapfval  35369  aomclem8  35832  islnm  35848  sdrgacs  35980  ioodvbdlimc1lem1  37686  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem1OLD  37688  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  iccpartiltu  38549  iccelpart  38560  nbgr2vtx1edg  39154  nbuhgr2vtx1edgb  39156  uvtxaval  39190  uvtxael  39191  uvtxael1  39198  uvtxusgrel  39206  iscplgr  39210  cusgredg  39220  cplgr3v  39230  cplgrop  39232  usgredgsscusgredg  39248  mgmpropd  39366  ismgmd  39367  ismgmhm  39374  resmgmhm  39389  iscllaw  39416  iscomlaw  39417  isasslaw  39419  isrng  39467  c0snmgmhm  39505  zlidlring  39519  uzlidlring  39520  dmatALTval  39786  islininds  39832  lindslinindsimp2  39849  ldepsnlinc  39894  elbigo  39955
  Copyright terms: Public domain W3C validator