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

Theorem raleqbi1dv 2923
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 2915 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
2 raleqd.1 . . 3  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
32ralbidv 2733 . 2  |-  ( A  =  B  ->  ( A. x  e.  B  ph  <->  A. x  e.  B  ps ) )
41, 3bitrd 253 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1364   A.wral 2713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718
This theorem is referenced by:  isoeq4  6010  smo11  6821  dffi2  7669  inficl  7671  dffi3  7677  dfom3  7849  aceq1  8283  dfac5lem4  8292  kmlem1  8315  kmlem10  8324  kmlem13  8327  kmlem14  8328  cofsmo  8434  infpssrlem4  8471  axdc3lem2  8616  elwina  8849  elina  8850  iswun  8867  eltskg  8913  elgrug  8955  elnp  9152  elnpi  9153  dfnn2  10331  dfnn3  10332  dfuzi  10728  ismri  14565  isprs  15096  isdrs  15100  ispos  15113  istos  15201  pospropd  15300  isipodrs  15327  isdlat  15359  mhmpropd  15466  issubm  15470  subgacs  15709  nsgacs  15710  isghm  15740  ghmeql  15762  iscmn  16277  dfrhm2  16798  islss  16994  lssacs  17026  lmhmeql  17114  islbs  17135  lbsextlem1  17217  lbsextlem3  17219  lbsextlem4  17220  isobs  18104  istopg  18467  isbasisg  18511  basis2  18515  eltg2  18522  iscldtop  18658  neipeltop  18692  isreg  18895  regsep  18897  isnrm  18898  islly  19031  isnlly  19032  llyi  19037  nllyi  19038  islly2  19047  cldllycmp  19058  isfbas  19361  fbssfi  19369  isust  19737  elutop  19767  ustuqtop  19780  utopsnneip  19782  ispsmet  19839  ismet  19857  isxmet  19858  metrest  20058  cncfval  20423  fmcfil  20742  iscfil3  20743  caucfil  20753  iscmet3  20763  cfilres  20766  minveclem3  20875  wilthlem2  22366  wilthlem3  22367  wilth  22368  isplig  23599  isgrpo  23618  isablo  23705  ismndo2  23767  rngomndo  23843  disjabrex  25861  disjabrexf  25862  isomnd  26097  isorng  26202  isrnsigaOLD  26491  isrnsiga  26492  kur14lem9  27032  cvmscbv  27077  cvmsi  27084  cvmsval  27085  wfrlem1  27653  wfrlem4  27656  wfrlem15  27667  frrlem1  27697  frrlem4  27700  neibastop1  28505  neibastop2lem  28506  neibastop2  28507  isbnd  28604  isidl  28739  isnacs  28965  mzpclval  28986  elmzpcl  28987  isfrgra  30507  bnj1286  31844  bnj1452  31877  ispsubsp  33111
  Copyright terms: Public domain W3C validator