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

Theorem raleqbidv 2918
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 2912 . 2  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43ralbidv 2727 . 2  |-  ( ph  ->  ( A. x  e.  B  ps  <->  A. x  e.  B  ch )
)
52, 4bitrd 246 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653   A.wral 2707
This theorem is referenced by:  knatar  6083  ofrfval  6316  fmpt2x  6420  ovmptss  6431  marypha1lem  7441  supeq123d  7458  oieq1  7484  acneq  7929  isfin1a  8177  fpwwe2cbv  8510  fpwwe2lem2  8512  fpwwecbv  8524  fpwwelem  8525  eltskg  8630  elgrug  8672  cau3lem  12163  rlim  12294  ello1  12314  elo1  12325  caurcvg2  12476  caucvgb  12478  fsum2dlem  12559  fsumcom2  12563  pcfac  13273  vdwpc  13353  rami  13388  prdsval  13683  ismre  13820  isacs2  13883  acsfiel  13884  iscat  13902  iscatd  13903  catidex  13904  catideu  13905  cidfval  13906  cidval  13907  catlid  13913  catrid  13914  comfeq  13937  catpropd  13940  monfval  13963  issubc  14040  fullsubc  14052  isfunc  14066  funcpropd  14102  isfull  14112  isfth  14116  fthpropd  14123  natfval  14148  isposd  14417  lubfval  14440  glbfval  14445  islat  14481  spwval2  14661  isla  14670  ismnd  14697  grpidval  14712  ismndd  14724  mndpropd  14726  ismhm  14745  resmhm  14764  gsumvalx  14779  gsumpropd  14781  gsumress  14782  isgrp  14821  grppropd  14828  isgrpd2e  14832  isnsg  14974  nmznsg  14989  isghm  15011  isga  15073  subgga  15082  gexval  15217  ispgp  15231  isslw  15247  sylow2blem2  15260  efgval  15354  efgi  15356  efgsdm  15367  cmnpropd  15426  iscmnd  15429  submcmn2  15463  gsumzaddlem  15531  dmdprd  15564  dprdcntz  15571  isrng  15673  rngpropd  15700  isirred  15809  abvfval  15911  abvpropd  15935  islmod  15959  islmodd  15961  lmodprop2d  16011  lssset  16015  islmhm  16108  reslmhm  16133  lmhmpropd  16150  islbs  16153  rrgval  16352  isdomn  16359  isassa  16380  isassad  16387  assapropd  16391  ltbval  16537  opsrval  16540  isphl  16864  istopg  16973  restbas  17227  ordtrest2  17273  cnfval  17302  cnpfval  17303  ist0  17389  ishaus  17391  iscnrm  17392  isnrm  17404  ist0-2  17413  ishaus2  17420  nrmsep3  17424  iscmp  17456  is1stc  17509  kgenval  17572  kgencn2  17594  txbas  17604  ptval  17607  dfac14  17655  isfil  17884  isufil  17940  isufl  17950  ucnval  18312  iscusp  18334  prdsxmslem2  18564  isnlm  18716  nmofval  18753  lebnumii  18996  iscau4  19237  iscmet  19242  iscmet3lem1  19249  iscmet3  19251  equivcmet  19273  ulmcaulem  20315  ulmcau  20316  fsumdvdscom  20975  dchrisumlem3  21190  pntibndlem2  21290  pntibnd  21292  pntlemp  21309  ostth2lem2  21333  iscusgra  21470  cusgrarn  21473  cusgra1v  21475  cusgra2v  21476  cusgra3v  21478  usgrasscusgra  21497  isuvtx  21502  uvtxel  21503  cusgrauvtxb  21510  iswlk  21532  istrl  21542  constr3trllem2  21643  isconngra  21664  isconngra1  21665  isplig  21770  gidval  21806  isgrp2d  21828  isgrpda  21890  isass  21909  isexid  21910  elghomlem1  21954  isrngo  21971  isrngod  21972  iscom2  22005  vci  22032  isvclem  22061  isnvlem  22094  lnoval  22258  ajfval  22315  isphg  22323  minvecolem3  22383  htth  22426  fmcncfil  24322  issiga  24499  isrnsigaOLD  24500  isrnsiga  24501  ismeas  24558  issibf  24653  sitgfval  24660  ispcon  24915  isscon  24918  txpcon  24924  cvxpcon  24934  cvmscbv  24950  iscvm  24951  cvmsdisj  24962  cvmsss2  24966  snmlval  25023  fprod2dlem  25309  fprodcom2  25313  isptfin  26389  islocfin  26390  cover2g  26430  seqpo  26465  incsequz2  26467  caushft  26481  ismtyval  26523  rngohomval  26594  idlval  26637  pridlval  26657  maxidlval  26663  aomclem8  27150  islnm  27166  islindf  27273  islindf2  27275  lsslindf  27291  sdrgacs  27500  f12dfv  28098  f13dfv  28099  wlkelwrd  28333  iswwlk  28365  wlkiswwlk2  28379  isrgra  28441  isfrgra  28454  frgraunss  28459  frgra1v  28462  frgra3v  28466  1vwmgra  28467  3vfriswmgra  28469  3cyclfrgrarn1  28476  n4cyclfrgra  28482  frgrancvvdeqlem4  28496  frgrawopreglem4  28510  frgrawopreg2  28514  frgraregorufr0  28515  lflset  29931  islfld  29934  isopos  30052  isoml  30110  isatl  30171  iscvlat  30195  ishlat1  30224  psubspset  30615  lautset  30953  pautsetN  30969  ldilfset  30979  ltrnfset  30988  dilfsetN  31023  trnfsetN  31026  trnsetN  31027  trlfset  31031  tendofset  31629  tendoset  31630  dihffval  32102  lpolsetN  32354  hdmapfval  32702  hgmapfval  32761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712
  Copyright terms: Public domain W3C validator