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

Theorem raleqbi1dv 3062
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)
Hypothesis
Ref Expression
raleqd.1  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
raleqbi1dv  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ps ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hints:    ph( x)    ps( x)

Proof of Theorem raleqbi1dv
StepHypRef Expression
1 raleq 3054 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
2 raleqd.1 . . 3  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
32ralbidv 2896 . 2  |-  ( A  =  B  ->  ( A. x  e.  B  ph  <->  A. x  e.  B  ps ) )
41, 3bitrd 253 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1395   A.wral 2807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812
This theorem is referenced by:  isoeq4  6219  smo11  7053  dffi2  7901  inficl  7903  dffi3  7909  dfom3  8081  aceq1  8515  dfac5lem4  8524  kmlem1  8547  kmlem10  8556  kmlem13  8559  kmlem14  8560  cofsmo  8666  infpssrlem4  8703  axdc3lem2  8848  elwina  9081  elina  9082  iswun  9099  eltskg  9145  elgrug  9187  elnp  9382  elnpi  9383  dfnn2  10569  dfnn3  10570  dfuzi  10974  ismri  15047  isprs  15685  isdrs  15689  ispos  15702  istos  15791  pospropd  15890  isipodrs  15917  isdlat  15949  mhmpropd  16098  issubm  16104  subgacs  16362  nsgacs  16363  isghm  16393  ghmeql  16415  iscmn  16931  dfrhm2  17492  islss  17707  lssacs  17739  lmhmeql  17827  islbs  17848  lbsextlem1  17930  lbsextlem3  17932  lbsextlem4  17933  isobs  18877  mat0dimcrng  19098  istopg  19530  isbasisg  19574  basis2  19578  eltg2  19585  iscldtop  19722  neipeltop  19756  isreg  19959  regsep  19961  isnrm  19962  islly  20094  isnlly  20095  llyi  20100  nllyi  20101  islly2  20110  cldllycmp  20121  isfbas  20455  fbssfi  20463  isust  20831  elutop  20861  ustuqtop  20874  utopsnneip  20876  ispsmet  20933  ismet  20951  isxmet  20952  metrest  21152  cncfval  21517  fmcfil  21836  iscfil3  21837  caucfil  21847  iscmet3  21857  cfilres  21860  minveclem3  21969  wilthlem2  23468  wilthlem3  23469  wilth  23470  isfrgra  25116  isplig  25305  isgrpo  25324  isablo  25411  ismndo2  25473  rngomndo  25549  disjabrex  27580  disjabrexf  27581  isomnd  27843  isorng  27942  isrnsigaOLD  28273  isrnsiga  28274  kur14lem9  28833  cvmscbv  28878  cvmsi  28885  cvmsval  28886  wfrlem1  29517  wfrlem4  29520  wfrlem15  29531  frrlem1  29561  frrlem4  29564  neibastop1  30339  neibastop2lem  30340  neibastop2  30341  isbnd  30438  isidl  30573  isnacs  30798  mzpclval  30819  elmzpcl  30820  mgmhmpropd  32693  issubmgm  32697  rnghmval  32799  zrrnghm  32825  bnj1286  34176  bnj1452  34209  ispsubsp  35570
  Copyright terms: Public domain W3C validator