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

Theorem raleqbidv 2876
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 2870 . 2  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ps )
)
3 raleqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
43ralbidv 2686 . 2  |-  ( ph  ->  ( A. x  e.  B  ps  <->  A. x  e.  B  ch )
)
52, 4bitrd 245 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   A.wral 2666
This theorem is referenced by:  knatar  6039  ofrfval  6272  fmpt2x  6376  ovmptss  6387  marypha1lem  7396  oieq1  7437  acneq  7880  isfin1a  8128  fpwwe2cbv  8461  fpwwe2lem2  8463  fpwwecbv  8475  fpwwelem  8476  eltskg  8581  elgrug  8623  cau3lem  12113  rlim  12244  ello1  12264  elo1  12275  caurcvg2  12426  caucvgb  12428  fsum2dlem  12509  fsumcom2  12513  pcfac  13223  vdwpc  13303  rami  13338  prdsval  13633  ismre  13770  isacs2  13833  acsfiel  13834  iscat  13852  iscatd  13853  catidex  13854  catideu  13855  cidfval  13856  cidval  13857  catlid  13863  catrid  13864  comfeq  13887  catpropd  13890  monfval  13913  issubc  13990  fullsubc  14002  isfunc  14016  funcpropd  14052  isfull  14062  isfth  14066  fthpropd  14073  natfval  14098  isposd  14367  lubfval  14390  glbfval  14395  islat  14431  spwval2  14611  isla  14620  ismnd  14647  grpidval  14662  ismndd  14674  mndpropd  14676  ismhm  14695  resmhm  14714  gsumvalx  14729  gsumpropd  14731  gsumress  14732  isgrp  14771  grppropd  14778  isgrpd2e  14782  isnsg  14924  nmznsg  14939  isghm  14961  isga  15023  subgga  15032  gexval  15167  ispgp  15181  isslw  15197  sylow2blem2  15210  efgval  15304  efgi  15306  efgsdm  15317  cmnpropd  15376  iscmnd  15379  submcmn2  15413  gsumzaddlem  15481  dmdprd  15514  dprdcntz  15521  isrng  15623  rngpropd  15650  isirred  15759  abvfval  15861  abvpropd  15885  islmod  15909  islmodd  15911  lmodprop2d  15961  lssset  15965  islmhm  16058  reslmhm  16083  lmhmpropd  16100  islbs  16103  rrgval  16302  isdomn  16309  isassa  16330  isassad  16337  assapropd  16341  ltbval  16487  opsrval  16490  isphl  16814  istopg  16923  restbas  17176  ordtrest2  17222  cnfval  17251  cnpfval  17252  ist0  17338  ishaus  17340  iscnrm  17341  isnrm  17353  ist0-2  17362  ishaus2  17369  nrmsep3  17373  iscmp  17405  is1stc  17457  kgenval  17520  kgencn2  17542  txbas  17552  ptval  17555  dfac14  17603  isfil  17832  isufil  17888  isufl  17898  ucnval  18260  iscusp  18282  prdsxmslem2  18512  isnlm  18664  nmofval  18701  lebnumii  18944  iscau4  19185  iscmet  19190  iscmet3lem1  19197  iscmet3  19199  equivcmet  19221  ulmcaulem  20263  ulmcau  20264  fsumdvdscom  20923  dchrisumlem3  21138  pntibndlem2  21238  pntibnd  21240  pntlemp  21257  ostth2lem2  21281  iscusgra  21418  cusgrarn  21421  cusgra1v  21423  cusgra2v  21424  cusgra3v  21426  usgrasscusgra  21445  isuvtx  21450  uvtxel  21451  cusgrauvtxb  21458  iswlk  21480  istrl  21490  constr3trllem2  21591  isconngra  21612  isconngra1  21613  isplig  21718  gidval  21754  isgrp2d  21776  isgrpda  21838  isass  21857  isexid  21858  elghomlem1  21902  isrngo  21919  isrngod  21920  iscom2  21953  vci  21980  isvclem  22009  isnvlem  22042  lnoval  22206  ajfval  22263  isphg  22271  minvecolem3  22331  htth  22374  fmcncfil  24270  issiga  24447  isrnsigaOLD  24448  isrnsiga  24449  ismeas  24506  issibf  24601  sitgfval  24608  ispcon  24863  isscon  24866  txpcon  24872  cvxpcon  24882  cvmscbv  24898  iscvm  24899  cvmsdisj  24910  cvmsss2  24914  snmlval  24971  fprod2dlem  25257  fprodcom2  25261  isptfin  26265  islocfin  26266  cover2g  26306  seqpo  26341  incsequz2  26343  caushft  26357  ismtyval  26399  rngohomval  26470  idlval  26513  pridlval  26533  maxidlval  26539  supeq123d  27026  aomclem8  27027  islnm  27043  islindf  27150  islindf2  27152  lsslindf  27168  sdrgacs  27377  f12dfv  27961  f13dfv  27962  isfrgra  28094  frgraunss  28099  frgra1v  28102  frgra3v  28106  1vwmgra  28107  3vfriswmgra  28109  3cyclfrgrarn1  28116  n4cyclfrgra  28122  frgrancvvdeqlem4  28136  frgrawopreglem4  28150  frgrawopreg2  28154  frgraregorufr0  28155  lflset  29542  islfld  29545  isopos  29663  isoml  29721  isatl  29782  iscvlat  29806  ishlat1  29835  psubspset  30226  lautset  30564  pautsetN  30580  ldilfset  30590  ltrnfset  30599  dilfsetN  30634  trnfsetN  30637  trnsetN  30638  trlfset  30642  tendofset  31240  tendoset  31241  dihffval  31713  lpolsetN  31965  hdmapfval  32313  hgmapfval  32372
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671
  Copyright terms: Public domain W3C validator