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

Theorem inteq 4053
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 2904 . . 3  |-  ( A  =  B  ->  ( A. y  e.  A  x  e.  y  <->  A. y  e.  B  x  e.  y ) )
21abbidv 2550 . 2  |-  ( A  =  B  ->  { x  |  A. y  e.  A  x  e.  y }  =  { x  |  A. y  e.  B  x  e.  y } )
3 dfint2 4052 . 2  |-  |^| A  =  { x  |  A. y  e.  A  x  e.  y }
4 dfint2 4052 . 2  |-  |^| B  =  { x  |  A. y  e.  B  x  e.  y }
52, 3, 43eqtr4g 2493 1  |-  ( A  =  B  ->  |^| A  =  |^| B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   {cab 2422   A.wral 2705   |^|cint 4050
This theorem is referenced by:  inteqi  4054  inteqd  4055  unissint  4074  uniintsn  4087  rint0  4090  intex  4356  intnex  4357  elreldm  5094  elxp5  5358  1stval2  6364  oev2  6767  fundmen  7180  xpsnen  7192  fiint  7383  elfir  7420  inelfi  7423  fiin  7427  cardmin2  7885  isfin2-2  8199  incexclem  12616  xpnnenOLD  12809  mreintcl  13820  ismred2  13828  fiinopn  16974  cmpfii  17472  ptbasfi  17613  fbssint  17870  shintcl  22832  chintcl  22834  rankeq1o  26112  neificl  26459  heibor1lem  26518  elrfi  26748  elrfirn  26749
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 2417
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-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2710  df-int 4051
  Copyright terms: Public domain W3C validator