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

Theorem raleqbidv 3054
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 3046 . 2  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43ralbidv 2882 . 2  |-  ( ph  ->  ( A. x  e.  B  ps  <->  A. x  e.  B  ch )
)
52, 4bitrd 253 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1383   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798
This theorem is referenced by:  f12dfv  6164  f13dfv  6165  knatar  6238  ofrfval  6533  fmpt2x  6851  ovmptss  6866  marypha1lem  7895  supeq123d  7912  oieq1  7940  acneq  8427  isfin1a  8675  fpwwe2cbv  9011  fpwwe2lem2  9013  fpwwecbv  9025  fpwwelem  9026  eltskg  9131  elgrug  9173  cau3lem  13168  rlim  13299  ello1  13319  elo1  13330  caurcvg2  13481  caucvgb  13483  fsum2dlem  13566  fsumcom2  13570  fprod2dlem  13765  fprodcom2  13769  pcfac  14399  vdwpc  14479  rami  14514  prdsval  14833  ismre  14968  isacs2  15031  acsfiel  15032  iscat  15050  iscatd  15051  catidex  15052  catideu  15053  cidfval  15054  cidval  15055  catlid  15061  catrid  15062  comfeq  15082  catpropd  15085  monfval  15108  issubc  15185  fullsubc  15197  isfunc  15211  funcpropd  15247  isfull  15257  isfth  15261  fthpropd  15268  natfval  15293  isposd  15563  lubfval  15586  glbfval  15599  ismgm  15851  grpidval  15865  gsumvalx  15875  gsumpropd  15877  gsumress  15881  issgrp  15890  ismnddef  15900  ismndOLD  15904  ismndd  15921  mndpropd  15924  ismhm  15946  resmhm  15968  isgrp  16039  grppropd  16046  isgrpd2e  16050  isnsg  16208  nmznsg  16223  isghm  16245  isga  16307  subgga  16316  gsmsymgrfix  16431  gsmsymgreq  16435  gexval  16576  ispgp  16590  isslw  16606  sylow2blem2  16619  efgval  16713  efgi  16715  efgsdm  16726  cmnpropd  16785  iscmnd  16788  submcmn2  16825  gsumzaddlem  16912  gsumzaddlemOLD  16914  dmdprd  17007  dprdcntz  17019  issrg  17137  isring  17180  ringpropd  17208  isirred  17326  abvfval  17445  abvpropd  17469  islmod  17494  islmodd  17496  lmodprop2d  17550  lssset  17558  islmhm  17651  reslmhm  17676  lmhmpropd  17697  islbs  17700  rrgval  17913  isdomn  17921  isassa  17942  isassad  17950  assapropd  17954  ltbval  18114  opsrval  18117  psgndiflemA  18614  isphl  18640  islindf  18824  islindf2  18826  lsslindf  18842  dmatval  18971  dmatcrng  18981  scmatcrng  19000  cpmat  19187  istopg  19381  restbas  19636  ordtrest2  19682  cnfval  19711  cnpfval  19712  ist0  19798  ishaus  19800  iscnrm  19801  isnrm  19813  ist0-2  19822  ishaus2  19829  nrmsep3  19833  iscmp  19865  is1stc  19919  isptfin  19994  islocfin  19995  kgenval  20013  kgencn2  20035  txbas  20045  ptval  20048  dfac14  20096  isfil  20325  isufil  20381  isufl  20391  ucnval  20757  iscusp  20779  prdsxmslem2  21009  isnlm  21161  nmofval  21198  lebnumii  21443  iscau4  21695  iscmet  21700  iscmet3lem1  21707  iscmet3  21709  equivcmet  21731  ulmcaulem  22765  ulmcau  22766  fsumdvdscom  23437  dchrisumlem3  23652  pntibndlem2  23752  pntibnd  23754  pntlemp  23771  ostth2lem2  23795  istrkg2d  23832  trgcgrg  23882  isismt  23897  iscusgra  24432  cusgrarn  24435  cusgra1v  24437  cusgra2v  24438  cusgra3v  24440  usgrasscusgra  24459  isuvtx  24464  uvtxel  24465  cusgrauvtxb  24472  iswlk  24496  wlkelwrd  24506  istrl  24515  constr3trllem2  24627  isconngra  24648  isconngra1  24649  iswwlk  24659  wlkiswwlk2  24673  isclwwlk  24744  clwwlkprop  24746  clwlkisclwwlklem2  24762  isrgra  24902  isfrgra  24966  frgraunss  24971  frgra1v  24974  frgra2v  24975  frgra3v  24978  1vwmgra  24979  3vfriswmgra  24981  3cyclfrgrarn1  24988  n4cyclfrgra  24994  frgrancvvdeqlem4  25009  frgrawopreglem4  25023  frgrawopreg2  25027  frgraregorufr0  25028  isplig  25155  gidval  25191  isgrp2d  25213  isgrpda  25275  isass  25294  isexid  25295  elghomlem1OLD  25339  isrngo  25356  isrngod  25357  iscom2  25390  vci  25417  isvclem  25446  isnvlem  25479  lnoval  25643  ajfval  25700  isphg  25708  minvecolem3  25768  htth  25811  ressprs  27620  isslmd  27722  resv1r  27804  iscref  27824  ordtrest2NEW  27882  fmcncfil  27890  issiga  28088  isrnsigaOLD  28089  isrnsiga  28090  ismeas  28147  issibf  28252  sitgfval  28260  signstfvneq0  28506  ispcon  28645  isscon  28648  txpcon  28654  cvxpcon  28664  cvmscbv  28680  iscvm  28681  cvmsdisj  28692  cvmsss2  28696  snmlval  28753  elmrsubrn  28857  ismfs  28886  mclsval  28900  cover2g  30180  seqpo  30215  incsequz2  30217  caushft  30229  ismtyval  30271  rngohomval  30342  idlval  30385  pridlval  30405  maxidlval  30411  aomclem8  30982  islnm  30998  sdrgacs  31126  ioodvbdlimc1lem1  31632  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  mgmpropd  32301  ismgmd  32302  ismgmhm  32309  resmgmhm  32324  iscllaw  32350  iscomlaw  32351  isasslaw  32353  isrng  32403  zlidlring  32444  uzlidlring  32445  dmatALTval  32736  islininds  32782  lindslinindsimp2  32799  ldepsnlinc  32844  lflset  34524  islfld  34527  isopos  34645  isoml  34703  isatl  34764  iscvlat  34788  ishlat1  34817  psubspset  35208  lautset  35546  pautsetN  35562  ldilfset  35572  ltrnfset  35581  dilfsetN  35617  trnfsetN  35620  trnsetN  35621  trlfset  35625  tendofset  36224  tendoset  36225  dihffval  36697  lpolsetN  36949  hdmapfval  37297  hgmapfval  37356
  Copyright terms: Public domain W3C validator