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

Theorem raleqbi1dv 2940
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 2932 . 2  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
2 raleqd.1 . . 3  |-  ( A  =  B  ->  ( ph 
<->  ps ) )
32ralbidv 2750 . 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 1369   A.wral 2730
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ral 2735
This theorem is referenced by:  isoeq4  6028  smo11  6840  dffi2  7688  inficl  7690  dffi3  7696  dfom3  7868  aceq1  8302  dfac5lem4  8311  kmlem1  8334  kmlem10  8343  kmlem13  8346  kmlem14  8347  cofsmo  8453  infpssrlem4  8490  axdc3lem2  8635  elwina  8868  elina  8869  iswun  8886  eltskg  8932  elgrug  8974  elnp  9171  elnpi  9172  dfnn2  10350  dfnn3  10351  dfuzi  10747  ismri  14584  isprs  15115  isdrs  15119  ispos  15132  istos  15220  pospropd  15319  isipodrs  15346  isdlat  15378  mhmpropd  15485  issubm  15490  subgacs  15731  nsgacs  15732  isghm  15762  ghmeql  15784  iscmn  16299  dfrhm2  16823  islss  17031  lssacs  17063  lmhmeql  17151  islbs  17172  lbsextlem1  17254  lbsextlem3  17256  lbsextlem4  17257  isobs  18160  istopg  18523  isbasisg  18567  basis2  18571  eltg2  18578  iscldtop  18714  neipeltop  18748  isreg  18951  regsep  18953  isnrm  18954  islly  19087  isnlly  19088  llyi  19093  nllyi  19094  islly2  19103  cldllycmp  19114  isfbas  19417  fbssfi  19425  isust  19793  elutop  19823  ustuqtop  19836  utopsnneip  19838  ispsmet  19895  ismet  19913  isxmet  19914  metrest  20114  cncfval  20479  fmcfil  20798  iscfil3  20799  caucfil  20809  iscmet3  20819  cfilres  20822  minveclem3  20931  wilthlem2  22422  wilthlem3  22423  wilth  22424  isplig  23679  isgrpo  23698  isablo  23785  ismndo2  23847  rngomndo  23923  disjabrex  25941  disjabrexf  25942  isomnd  26179  isorng  26282  isrnsigaOLD  26570  isrnsiga  26571  kur14lem9  27117  cvmscbv  27162  cvmsi  27169  cvmsval  27170  wfrlem1  27739  wfrlem4  27742  wfrlem15  27753  frrlem1  27783  frrlem4  27786  neibastop1  28599  neibastop2lem  28600  neibastop2  28601  isbnd  28698  isidl  28833  isnacs  29059  mzpclval  29080  elmzpcl  29081  isfrgra  30601  bnj1286  32029  bnj1452  32062  ispsubsp  33408
  Copyright terms: Public domain W3C validator