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

Theorem raleqbi1dv 2872
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 2864 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
2 raleqd.1 . . 3  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
32ralbidv 2686 . 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 2666
This theorem is referenced by:  isoeq4  6001  smo11  6585  dffi2  7386  inficl  7388  dffi3  7394  dfom3  7558  aceq1  7954  dfac5lem4  7963  kmlem1  7986  kmlem10  7995  kmlem13  7998  kmlem14  7999  cofsmo  8105  infpssrlem4  8142  axdc3lem2  8287  elwina  8517  elina  8518  iswun  8535  eltskg  8581  elgrug  8623  elnp  8820  elnpi  8821  dfnn2  9969  dfnn3  9970  dfuzi  10316  ismri  13811  isprs  14342  isdrs  14346  ispos  14359  istos  14419  pospropd  14516  isipodrs  14542  isdlat  14574  mhmpropd  14699  issubm  14703  subgacs  14930  nsgacs  14931  isghm  14961  ghmeql  14983  iscmn  15374  dfrhm2  15776  islss  15966  lssacs  15998  lmhmeql  16086  islbs  16103  lbsextlem1  16185  lbsextlem3  16187  lbsextlem4  16188  isobs  16902  istopg  16923  isbasisg  16967  basis2  16971  eltg2  16978  iscldtop  17114  neipeltop  17148  isreg  17350  regsep  17352  isnrm  17353  islly  17484  isnlly  17485  llyi  17490  nllyi  17491  islly2  17500  cldllycmp  17511  isfbas  17814  fbssfi  17822  isust  18186  elutop  18216  ustuqtop  18229  utopsnneip  18231  ispsmet  18288  ismet  18306  isxmet  18307  metrest  18507  cncfval  18871  fmcfil  19178  iscfil3  19179  caucfil  19189  iscmet3  19199  cfilres  19202  minveclem3  19283  wilthlem2  20805  wilthlem3  20806  wilth  20807  isplig  21718  isgrpo  21737  isablo  21824  ismndo2  21886  rngomndo  21962  disjabrex  23977  disjabrexf  23978  isofld  24188  isrnsigaOLD  24448  isrnsiga  24449  kur14lem9  24853  cvmscbv  24898  cvmsi  24905  cvmsval  24906  wfrlem1  25470  wfrlem4  25473  wfrlem15  25484  frrlem1  25495  frrlem4  25498  bpolyval  25999  neibastop1  26278  neibastop2lem  26279  neibastop2  26280  isbnd  26379  isidl  26514  isnacs  26648  mzpclval  26672  elmzpcl  26673  isfrgra  28094  bnj1286  29094  bnj1452  29127  ispsubsp  30227
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