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

Theorem raleqbi1dv 3066
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 3058 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
2 raleqd.1 . . 3  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
32ralbidv 2903 . 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 1379   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819
This theorem is referenced by:  isoeq4  6204  smo11  7032  dffi2  7879  inficl  7881  dffi3  7887  dfom3  8060  aceq1  8494  dfac5lem4  8503  kmlem1  8526  kmlem10  8535  kmlem13  8538  kmlem14  8539  cofsmo  8645  infpssrlem4  8682  axdc3lem2  8827  elwina  9060  elina  9061  iswun  9078  eltskg  9124  elgrug  9166  elnp  9361  elnpi  9362  dfnn2  10545  dfnn3  10546  dfuzi  10947  ismri  14882  isprs  15413  isdrs  15417  ispos  15430  istos  15518  pospropd  15617  isipodrs  15644  isdlat  15676  mhmpropd  15783  issubm  15788  subgacs  16031  nsgacs  16032  isghm  16062  ghmeql  16084  iscmn  16601  dfrhm2  17150  islss  17364  lssacs  17396  lmhmeql  17484  islbs  17505  lbsextlem1  17587  lbsextlem3  17589  lbsextlem4  17590  isobs  18518  istopg  19171  isbasisg  19215  basis2  19219  eltg2  19226  iscldtop  19362  neipeltop  19396  isreg  19599  regsep  19601  isnrm  19602  islly  19735  isnlly  19736  llyi  19741  nllyi  19742  islly2  19751  cldllycmp  19762  isfbas  20065  fbssfi  20073  isust  20441  elutop  20471  ustuqtop  20484  utopsnneip  20486  ispsmet  20543  ismet  20561  isxmet  20562  metrest  20762  cncfval  21127  fmcfil  21446  iscfil3  21447  caucfil  21457  iscmet3  21467  cfilres  21470  minveclem3  21579  wilthlem2  23071  wilthlem3  23072  wilth  23073  isfrgra  24666  isplig  24855  isgrpo  24874  isablo  24961  ismndo2  25023  rngomndo  25099  disjabrex  27116  disjabrexf  27117  isomnd  27353  isorng  27452  isrnsigaOLD  27752  isrnsiga  27753  kur14lem9  28298  cvmscbv  28343  cvmsi  28350  cvmsval  28351  wfrlem1  28920  wfrlem4  28923  wfrlem15  28934  frrlem1  28964  frrlem4  28967  neibastop1  29780  neibastop2lem  29781  neibastop2  29782  isbnd  29879  isidl  30014  isnacs  30240  mzpclval  30261  elmzpcl  30262  bnj1286  33154  bnj1452  33187  ispsubsp  34541
  Copyright terms: Public domain W3C validator