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

Theorem raleqbi1dv 2904
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 2896 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
2 raleqd.1 . . 3  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
32ralbidv 2717 . 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 1652   A.wral 2697
This theorem is referenced by:  isoeq4  6034  smo11  6618  dffi2  7420  inficl  7422  dffi3  7428  dfom3  7594  aceq1  7990  dfac5lem4  7999  kmlem1  8022  kmlem10  8031  kmlem13  8034  kmlem14  8035  cofsmo  8141  infpssrlem4  8178  axdc3lem2  8323  elwina  8553  elina  8554  iswun  8571  eltskg  8617  elgrug  8659  elnp  8856  elnpi  8857  dfnn2  10005  dfnn3  10006  dfuzi  10352  ismri  13848  isprs  14379  isdrs  14383  ispos  14396  istos  14456  pospropd  14553  isipodrs  14579  isdlat  14611  mhmpropd  14736  issubm  14740  subgacs  14967  nsgacs  14968  isghm  14998  ghmeql  15020  iscmn  15411  dfrhm2  15813  islss  16003  lssacs  16035  lmhmeql  16123  islbs  16140  lbsextlem1  16222  lbsextlem3  16224  lbsextlem4  16225  isobs  16939  istopg  16960  isbasisg  17004  basis2  17008  eltg2  17015  iscldtop  17151  neipeltop  17185  isreg  17388  regsep  17390  isnrm  17391  islly  17523  isnlly  17524  llyi  17529  nllyi  17530  islly2  17539  cldllycmp  17550  isfbas  17853  fbssfi  17861  isust  18225  elutop  18255  ustuqtop  18268  utopsnneip  18270  ispsmet  18327  ismet  18345  isxmet  18346  metrest  18546  cncfval  18910  fmcfil  19217  iscfil3  19218  caucfil  19228  iscmet3  19238  cfilres  19241  minveclem3  19322  wilthlem2  20844  wilthlem3  20845  wilth  20846  isplig  21757  isgrpo  21776  isablo  21863  ismndo2  21925  rngomndo  22001  disjabrex  24016  disjabrexf  24017  isofld  24227  isrnsigaOLD  24487  isrnsiga  24488  kur14lem9  24892  cvmscbv  24937  cvmsi  24944  cvmsval  24945  wfrlem1  25530  wfrlem4  25533  wfrlem15  25544  frrlem1  25574  frrlem4  25577  neibastop1  26379  neibastop2lem  26380  neibastop2  26381  isbnd  26480  isidl  26615  isnacs  26749  mzpclval  26773  elmzpcl  26774  isfrgra  28317  bnj1286  29325  bnj1452  29358  ispsubsp  30479
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702
  Copyright terms: Public domain W3C validator