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

Theorem raleqbi1dv 2744
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 2736 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
2 raleqd.1 . . 3  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
32ralbidv 2563 . 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 1623   A.wral 2543
This theorem is referenced by:  isoeq4  5819  smo11  6381  dffi2  7176  inficl  7178  dffi3  7184  dfom3  7348  aceq1  7744  dfac5lem4  7753  kmlem1  7776  kmlem10  7785  kmlem13  7788  kmlem14  7789  cofsmo  7895  infpssrlem4  7932  axdc3lem2  8077  elwina  8308  elina  8309  iswun  8326  eltskg  8372  elgrug  8414  elnp  8611  elnpi  8612  dfnn2  9759  dfnn3  9760  dfuzi  10102  ismri  13533  isprs  14064  isdrs  14068  ispos  14081  istos  14141  pospropd  14238  isipodrs  14264  isdlat  14296  mhmpropd  14421  issubm  14425  subgacs  14652  nsgacs  14653  isghm  14683  ghmeql  14705  iscmn  15096  dfrhm2  15498  islss  15692  lssacs  15724  lmhmeql  15812  islbs  15829  lbsextlem1  15911  lbsextlem3  15913  lbsextlem4  15914  isobs  16620  istopg  16641  isbasisg  16685  basis2  16689  eltg2  16696  iscldtop  16832  isreg  17060  regsep  17062  isnrm  17063  islly  17194  isnlly  17195  llyi  17200  nllyi  17201  islly2  17210  cldllycmp  17221  isfbas  17524  fbssfi  17532  ismet  17888  isxmet  17889  metrest  18070  cncfval  18392  fmcfil  18698  iscfil3  18699  caucfil  18709  iscmet3  18719  cfilres  18722  minveclem3  18793  wilthlem2  20307  wilthlem3  20308  wilth  20309  isplig  20844  isgrpo  20863  isablo  20950  ismndo2  21012  rngomndo  21088  disjabrex  23359  disjabrexf  23360  isrnsigaOLD  23473  isrnsiga  23474  kur14lem9  23745  cvmscbv  23789  cvmsi  23796  cvmsval  23797  wfrlem1  24256  wfrlem4  24259  wfrlem15  24270  frrlem1  24281  frrlem4  24284  bpolyval  24784  islatalg  25183  isdir2  25292  ablocomgrp  25342  com2i  25416  isidlNEW  25446  istopx  25547  tcnvec  25690  isibg2  26110  isibcg  26191  neibastop1  26308  neibastop2lem  26309  neibastop2  26310  isbnd  26504  isidl  26639  isnacs  26779  mzpclval  26803  elmzpcl  26804  isfrgra  28171  bnj1286  29049  bnj1452  29082  ispsubsp  29934
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548
  Copyright terms: Public domain W3C validator