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

Theorem raleqbi1dv 2855
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 2847 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
2 raleqd.1 . . 3  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
32ralbidv 2669 . 2  |-  ( A  =  B  ->  ( A. x  e.  B  ph  <->  A. x  e.  B  ps ) )
41, 3bitrd 245 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   A.wral 2649
This theorem is referenced by:  isoeq4  5981  smo11  6562  dffi2  7363  inficl  7365  dffi3  7371  dfom3  7535  aceq1  7931  dfac5lem4  7940  kmlem1  7963  kmlem10  7972  kmlem13  7975  kmlem14  7976  cofsmo  8082  infpssrlem4  8119  axdc3lem2  8264  elwina  8494  elina  8495  iswun  8512  eltskg  8558  elgrug  8600  elnp  8797  elnpi  8798  dfnn2  9945  dfnn3  9946  dfuzi  10292  ismri  13783  isprs  14314  isdrs  14318  ispos  14331  istos  14391  pospropd  14488  isipodrs  14514  isdlat  14546  mhmpropd  14671  issubm  14675  subgacs  14902  nsgacs  14903  isghm  14933  ghmeql  14955  iscmn  15346  dfrhm2  15748  islss  15938  lssacs  15970  lmhmeql  16058  islbs  16075  lbsextlem1  16157  lbsextlem3  16159  lbsextlem4  16160  isobs  16870  istopg  16891  isbasisg  16935  basis2  16939  eltg2  16946  iscldtop  17082  neipeltop  17116  isreg  17318  regsep  17320  isnrm  17321  islly  17452  isnlly  17453  llyi  17458  nllyi  17459  islly2  17468  cldllycmp  17479  isfbas  17782  fbssfi  17790  isust  18154  elutop  18184  ustuqtop  18197  utopsnneip  18199  ismet  18262  isxmet  18263  metrest  18444  cncfval  18789  fmcfil  19096  iscfil3  19097  caucfil  19107  iscmet3  19117  cfilres  19120  minveclem3  19197  wilthlem2  20719  wilthlem3  20720  wilth  20721  isplig  21613  isgrpo  21632  isablo  21719  ismndo2  21781  rngomndo  21857  disjabrex  23868  disjabrexf  23869  isofld  24061  isrnsigaOLD  24291  isrnsiga  24292  kur14lem9  24679  cvmscbv  24724  cvmsi  24731  cvmsval  24732  wfrlem1  25280  wfrlem4  25283  wfrlem15  25294  frrlem1  25305  frrlem4  25308  bpolyval  25809  neibastop1  26079  neibastop2lem  26080  neibastop2  26081  isbnd  26180  isidl  26315  isnacs  26449  mzpclval  26473  elmzpcl  26474  isfrgra  27743  bnj1286  28726  bnj1452  28759  ispsubsp  29859
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654
  Copyright terms: Public domain W3C validator