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

Theorem raleqbi1dv 2757
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 2749 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
2 raleqd.1 . . 3  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
32ralbidv 2576 . 2  |-  ( A  =  B  ->  ( A. x  e.  B  ph  <->  A. x  e.  B  ps ) )
41, 3bitrd 244 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   A.wral 2556
This theorem is referenced by:  isoeq4  5835  smo11  6397  dffi2  7192  inficl  7194  dffi3  7200  dfom3  7364  aceq1  7760  dfac5lem4  7769  kmlem1  7792  kmlem10  7801  kmlem13  7804  kmlem14  7805  cofsmo  7911  infpssrlem4  7948  axdc3lem2  8093  elwina  8324  elina  8325  iswun  8342  eltskg  8388  elgrug  8430  elnp  8627  elnpi  8628  dfnn2  9775  dfnn3  9776  dfuzi  10118  ismri  13549  isprs  14080  isdrs  14084  ispos  14097  istos  14157  pospropd  14254  isipodrs  14280  isdlat  14312  mhmpropd  14437  issubm  14441  subgacs  14668  nsgacs  14669  isghm  14699  ghmeql  14721  iscmn  15112  dfrhm2  15514  islss  15708  lssacs  15740  lmhmeql  15828  islbs  15845  lbsextlem1  15927  lbsextlem3  15929  lbsextlem4  15930  isobs  16636  istopg  16657  isbasisg  16701  basis2  16705  eltg2  16712  iscldtop  16848  isreg  17076  regsep  17078  isnrm  17079  islly  17210  isnlly  17211  llyi  17216  nllyi  17217  islly2  17226  cldllycmp  17237  isfbas  17540  fbssfi  17548  ismet  17904  isxmet  17905  metrest  18086  cncfval  18408  fmcfil  18714  iscfil3  18715  caucfil  18725  iscmet3  18735  cfilres  18738  minveclem3  18809  wilthlem2  20323  wilthlem3  20324  wilth  20325  isplig  20860  isgrpo  20879  isablo  20966  ismndo2  21028  rngomndo  21104  disjabrex  23374  disjabrexf  23375  isrnsigaOLD  23488  isrnsiga  23489  kur14lem9  23760  cvmscbv  23804  cvmsi  23811  cvmsval  23812  wfrlem1  24327  wfrlem4  24330  wfrlem15  24341  frrlem1  24352  frrlem4  24355  bpolyval  24856  islatalg  25286  isdir2  25395  ablocomgrp  25445  com2i  25519  isidlNEW  25549  istopx  25650  tcnvec  25793  isibg2  26213  isibcg  26294  neibastop1  26411  neibastop2lem  26412  neibastop2  26413  isbnd  26607  isidl  26742  isnacs  26882  mzpclval  26906  elmzpcl  26907  isfrgra  28417  bnj1286  29365  bnj1452  29398  ispsubsp  30556
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561
  Copyright terms: Public domain W3C validator