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

Theorem inteq 3995
Description: Equality law for intersection. (Contributed by NM, 13-Sep-1999.)
Assertion
Ref Expression
inteq  |-  ( A  =  B  ->  |^| A  =  |^| B )

Proof of Theorem inteq
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 raleq 2847 . . 3  |-  ( A  =  B  ->  ( A. y  e.  A  x  e.  y  <->  A. y  e.  B  x  e.  y ) )
21abbidv 2501 . 2  |-  ( A  =  B  ->  { x  |  A. y  e.  A  x  e.  y }  =  { x  |  A. y  e.  B  x  e.  y } )
3 dfint2 3994 . 2  |-  |^| A  =  { x  |  A. y  e.  A  x  e.  y }
4 dfint2 3994 . 2  |-  |^| B  =  { x  |  A. y  e.  B  x  e.  y }
52, 3, 43eqtr4g 2444 1  |-  ( A  =  B  ->  |^| A  =  |^| B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   {cab 2373   A.wral 2649   |^|cint 3992
This theorem is referenced by:  inteqi  3996  inteqd  3997  unissint  4016  uniintsn  4029  rint0  4032  intex  4297  intnex  4298  elreldm  5034  elxp5  5298  1stval2  6303  oev2  6703  fundmen  7116  xpsnen  7128  fiint  7319  elfir  7355  inelfi  7358  fiin  7362  cardmin2  7818  isfin2-2  8132  incexclem  12543  xpnnenOLD  12736  mreintcl  13747  ismred2  13755  fiinopn  16897  cmpfii  17394  ptbasfi  17534  fbssint  17791  shintcl  22680  chintcl  22682  rankeq1o  25826  neificl  26150  heibor1lem  26209  elrfi  26439  elrfirn  26440
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654  df-int 3993
  Copyright terms: Public domain W3C validator