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

Theorem raleqbi1dv 3007
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 2999 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
2 raleqd.1 . . 3  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
32ralbidv 2839 . 2  |-  ( A  =  B  ->  ( A. x  e.  B  ph  <->  A. x  e.  B  ps ) )
41, 3bitrd 261 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1455   A.wral 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754
This theorem is referenced by:  isoeq4  6238  wfrlem1  7061  wfrlem4  7065  wfrlem15  7076  smo11  7109  dffi2  7963  inficl  7965  dffi3  7971  dfom3  8178  aceq1  8574  dfac5lem4  8583  kmlem1  8606  kmlem10  8615  kmlem13  8618  kmlem14  8619  cofsmo  8725  infpssrlem4  8762  axdc3lem2  8907  elwina  9137  elina  9138  iswun  9155  eltskg  9201  elgrug  9243  elnp  9438  elnpi  9439  dfnn2  10650  dfnn3  10651  dfuzi  11055  coprmprod  14727  coprmproddvds  14729  ismri  15586  isprs  16224  isdrs  16228  ispos  16241  istos  16330  pospropd  16429  isipodrs  16456  isdlat  16488  mhmpropd  16637  issubm  16643  subgacs  16901  nsgacs  16902  isghm  16932  ghmeql  16954  iscmn  17486  dfrhm2  17994  islss  18207  lssacs  18239  lmhmeql  18327  islbs  18348  lbsextlem1  18430  lbsextlem3  18432  lbsextlem4  18433  isobs  19332  mat0dimcrng  19544  istopg  19974  isbasisg  20011  basis2  20015  eltg2  20022  iscldtop  20160  neipeltop  20194  isreg  20397  regsep  20399  isnrm  20400  islly  20532  isnlly  20533  llyi  20538  nllyi  20539  islly2  20548  cldllycmp  20559  isfbas  20893  fbssfi  20901  isust  21267  elutop  21297  ustuqtop  21310  utopsnneip  21312  ispsmet  21369  ismet  21387  isxmet  21388  metrest  21588  cncfval  21969  fmcfil  22291  iscfil3  22292  caucfil  22302  iscmet3  22312  cfilres  22315  minveclem3  22420  minveclem3OLD  22432  wilthlem2  24043  wilthlem3  24044  wilth  24045  isfrgra  25767  isplig  25958  isgrpo  25973  isablo  26060  ismndo2  26122  rngomndo  26198  disjabrex  28241  disjabrexf  28242  isomnd  28513  isorng  28611  isrnsigaOLD  28983  isrnsiga  28984  isldsys  29027  isros  29039  issros  29046  bnj1286  29877  bnj1452  29910  kur14lem9  29986  cvmscbv  30030  cvmsi  30037  cvmsval  30038  frrlem1  30563  frrlem4  30566  neibastop1  31064  neibastop2lem  31065  neibastop2  31066  isbnd  32157  isidl  32292  ispsubsp  33355  isnacs  35591  mzpclval  35612  elmzpcl  35613  dfconngr1  39929  mgmhmpropd  40058  issubmgm  40062  rnghmval  40164  zrrnghm  40190
  Copyright terms: Public domain W3C validator