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

Theorem raleqbi1dv 3031
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 3023 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
2 raleqd.1 . . 3  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
32ralbidv 2862 . 2  |-  ( A  =  B  ->  ( A. x  e.  B  ph  <->  A. x  e.  B  ps ) )
41, 3bitrd 256 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   A.wral 2773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ral 2778
This theorem is referenced by:  isoeq4  6219  wfrlem1  7034  wfrlem4  7038  wfrlem15  7049  smo11  7082  dffi2  7934  inficl  7936  dffi3  7942  dfom3  8143  aceq1  8537  dfac5lem4  8546  kmlem1  8569  kmlem10  8578  kmlem13  8581  kmlem14  8582  cofsmo  8688  infpssrlem4  8725  axdc3lem2  8870  elwina  9100  elina  9101  iswun  9118  eltskg  9164  elgrug  9206  elnp  9401  elnpi  9402  dfnn2  10611  dfnn3  10612  dfuzi  11015  coprmprod  14638  coprmproddvds  14640  ismri  15481  isprs  16119  isdrs  16123  ispos  16136  istos  16225  pospropd  16324  isipodrs  16351  isdlat  16383  mhmpropd  16532  issubm  16538  subgacs  16796  nsgacs  16797  isghm  16827  ghmeql  16849  iscmn  17365  dfrhm2  17873  islss  18086  lssacs  18118  lmhmeql  18206  islbs  18227  lbsextlem1  18309  lbsextlem3  18311  lbsextlem4  18312  isobs  19207  mat0dimcrng  19419  istopg  19849  isbasisg  19886  basis2  19890  eltg2  19897  iscldtop  20035  neipeltop  20069  isreg  20272  regsep  20274  isnrm  20275  islly  20407  isnlly  20408  llyi  20413  nllyi  20414  islly2  20423  cldllycmp  20434  isfbas  20768  fbssfi  20776  isust  21142  elutop  21172  ustuqtop  21185  utopsnneip  21187  ispsmet  21244  ismet  21262  isxmet  21263  metrest  21463  cncfval  21809  fmcfil  22128  iscfil3  22129  caucfil  22139  iscmet3  22149  cfilres  22152  minveclem3  22257  wilthlem2  23856  wilthlem3  23857  wilth  23858  isfrgra  25560  isplig  25751  isgrpo  25766  isablo  25853  ismndo2  25915  rngomndo  25991  disjabrex  28028  disjabrexf  28029  isomnd  28299  isorng  28398  isrnsigaOLD  28770  isrnsiga  28771  isldsys  28814  isros  28826  issros  28833  bnj1286  29613  bnj1452  29646  kur14lem9  29722  cvmscbv  29766  cvmsi  29773  cvmsval  29774  frrlem1  30298  frrlem4  30301  neibastop1  30797  neibastop2lem  30798  neibastop2  30799  isbnd  31816  isidl  31951  ispsubsp  33019  isnacs  35255  mzpclval  35276  elmzpcl  35277  mgmhmpropd  38556  issubmgm  38560  rnghmval  38662  zrrnghm  38688
  Copyright terms: Public domain W3C validator