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

Theorem raleqbidv 2993
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 2985 . 2  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43ralbidv 2821 . 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 1399   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-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ral 2737
This theorem is referenced by:  f12dfv  6080  f13dfv  6081  knatar  6154  ofrfval  6447  fmpt2x  6765  ovmptss  6780  marypha1lem  7808  supeq123d  7824  oieq1  7852  acneq  8337  isfin1a  8585  fpwwe2cbv  8919  fpwwe2lem2  8921  fpwwecbv  8933  fpwwelem  8934  eltskg  9039  elgrug  9081  cau3lem  13189  rlim  13320  ello1  13340  elo1  13351  caurcvg2  13502  caucvgb  13504  fsum2dlem  13587  fsumcom2  13591  fprod2dlem  13786  fprodcom2  13790  pcfac  14420  vdwpc  14500  rami  14535  prdsval  14862  ismre  14997  isacs2  15060  acsfiel  15061  iscat  15079  iscatd  15080  catidex  15081  catideu  15082  cidfval  15083  cidval  15084  catlid  15090  catrid  15091  comfeq  15112  catpropd  15115  monfval  15138  issubc  15241  fullsubc  15256  isfunc  15270  funcpropd  15306  isfull  15316  isfth  15320  fthpropd  15327  natfval  15352  initoval  15393  termoval  15394  isposd  15702  lubfval  15725  glbfval  15738  ismgm  15990  grpidval  16004  gsumvalx  16014  gsumpropd  16016  gsumress  16020  issgrp  16029  ismnddef  16039  ismndOLD  16043  ismndd  16060  mndpropd  16063  ismhm  16085  resmhm  16107  isgrp  16178  grppropd  16185  isgrpd2e  16189  isnsg  16347  nmznsg  16362  isghm  16384  isga  16446  subgga  16455  gsmsymgrfix  16570  gsmsymgreq  16574  gexval  16715  ispgp  16729  isslw  16745  sylow2blem2  16758  efgval  16852  efgi  16854  efgsdm  16865  cmnpropd  16924  iscmnd  16927  submcmn2  16964  gsumzaddlem  17051  gsumzaddlemOLD  17053  dmdprd  17142  dprdcntz  17154  issrg  17272  isring  17315  ringpropd  17343  isirred  17461  abvfval  17580  abvpropd  17604  islmod  17629  islmodd  17631  lmodprop2d  17685  lssset  17693  islmhm  17786  reslmhm  17811  lmhmpropd  17832  islbs  17835  rrgval  18048  isdomn  18056  isassa  18077  isassad  18085  assapropd  18089  ltbval  18249  opsrval  18252  psgndiflemA  18728  isphl  18754  islindf  18932  islindf2  18934  lsslindf  18950  dmatval  19079  dmatcrng  19089  scmatcrng  19108  cpmat  19295  istopg  19489  restbas  19745  ordtrest2  19791  cnfval  19820  cnpfval  19821  ist0  19907  ishaus  19909  iscnrm  19910  isnrm  19922  ist0-2  19931  ishaus2  19938  nrmsep3  19942  iscmp  19974  is1stc  20027  isptfin  20102  islocfin  20103  kgenval  20121  kgencn2  20143  txbas  20153  ptval  20156  dfac14  20204  isfil  20433  isufil  20489  isufl  20499  ucnval  20865  iscusp  20887  prdsxmslem2  21117  isnlm  21269  nmofval  21306  lebnumii  21551  iscau4  21803  iscmet  21808  iscmet3lem1  21815  iscmet3  21817  equivcmet  21839  ulmcaulem  22874  ulmcau  22875  fsumdvdscom  23578  dchrisumlem3  23793  pntibndlem2  23893  pntibnd  23895  pntlemp  23912  ostth2lem2  23936  istrkg2d  23973  trgcgrg  24026  isismt  24041  iscusgra  24577  cusgrarn  24580  cusgra1v  24582  cusgra2v  24583  cusgra3v  24585  usgrasscusgra  24604  isuvtx  24609  uvtxel  24610  cusgrauvtxb  24617  iswlk  24641  wlkelwrd  24651  istrl  24660  constr3trllem2  24772  isconngra  24793  isconngra1  24794  iswwlk  24804  wlkiswwlk2  24818  isclwwlk  24889  clwwlkprop  24891  clwlkisclwwlklem2  24907  isrgra  25047  isfrgra  25111  frgraunss  25116  frgra1v  25119  frgra2v  25120  frgra3v  25123  1vwmgra  25124  3vfriswmgra  25126  3cyclfrgrarn1  25133  n4cyclfrgra  25139  frgrancvvdeqlem4  25154  frgrawopreglem4  25168  frgrawopreg2  25172  frgraregorufr0  25173  isplig  25300  gidval  25332  isgrp2d  25354  isgrpda  25416  isass  25435  isexid  25436  elghomlem1OLD  25480  isrngo  25497  isrngod  25498  iscom2  25531  vci  25558  isvclem  25587  isnvlem  25620  lnoval  25784  ajfval  25841  isphg  25849  minvecolem3  25909  htth  25952  ressprs  27796  isslmd  27898  resv1r  27981  iscref  28001  ordtrest2NEW  28059  fmcncfil  28067  issiga  28260  isrnsigaOLD  28261  isrnsiga  28262  isldsys  28304  ismeas  28326  carsgval  28430  issibf  28458  sitgfval  28466  signstfvneq0  28712  ispcon  28857  isscon  28860  txpcon  28866  cvxpcon  28876  cvmscbv  28892  iscvm  28893  cvmsdisj  28904  cvmsss2  28908  snmlval  28965  elmrsubrn  29069  ismfs  29098  mclsval  29112  cover2g  30371  seqpo  30406  incsequz2  30408  caushft  30420  ismtyval  30462  rngohomval  30533  idlval  30576  pridlval  30596  maxidlval  30602  aomclem8  31173  islnm  31189  sdrgacs  31318  ioodvbdlimc1lem1  31894  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  mgmpropd  32781  ismgmd  32782  ismgmhm  32789  resmgmhm  32804  iscllaw  32831  iscomlaw  32832  isasslaw  32834  isrng  32882  c0snmgmhm  32920  zlidlring  32934  uzlidlring  32935  dmatALTval  33201  islininds  33247  lindslinindsimp2  33264  ldepsnlinc  33309  elbigo  33372  lflset  35197  islfld  35200  isopos  35318  isoml  35376  isatl  35437  iscvlat  35461  ishlat1  35490  psubspset  35881  lautset  36219  pautsetN  36235  ldilfset  36245  ltrnfset  36254  dilfsetN  36290  trnfsetN  36293  trnsetN  36294  trlfset  36298  tendofset  36897  tendoset  36898  dihffval  37370  lpolsetN  37622  hdmapfval  37970  hgmapfval  38029
  Copyright terms: Public domain W3C validator