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

Theorem inteq 3865
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 2736 . . 3  |-  ( A  =  B  ->  ( A. y  e.  A  x  e.  y  <->  A. y  e.  B  x  e.  y ) )
21abbidv 2397 . 2  |-  ( A  =  B  ->  { x  |  A. y  e.  A  x  e.  y }  =  { x  |  A. y  e.  B  x  e.  y } )
3 dfint2 3864 . 2  |-  |^| A  =  { x  |  A. y  e.  A  x  e.  y }
4 dfint2 3864 . 2  |-  |^| B  =  { x  |  A. y  e.  B  x  e.  y }
52, 3, 43eqtr4g 2340 1  |-  ( A  =  B  ->  |^| A  =  |^| B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   {cab 2269   A.wral 2543   |^|cint 3862
This theorem is referenced by:  inteqi  3866  inteqd  3867  unissint  3886  uniintsn  3899  rint0  3902  intex  4167  intnex  4168  elreldm  4903  elxp5  5161  1stval2  6137  oev2  6522  fundmen  6934  xpsnen  6946  fiint  7133  elfir  7169  fiin  7175  cardmin2  7631  isfin2-2  7945  incexclem  12295  incexc  12296  xpnnenOLD  12488  mreintcl  13497  ismred2  13505  fiinopn  16647  cmpfii  17136  ptbasfi  17276  fbssint  17533  shintcl  21909  chintcl  21911  rankeq1o  24801  isconcl2b  26098  neificl  26467  heibor1lem  26533  elrfi  26769  elrfirn  26770
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-int 3863
  Copyright terms: Public domain W3C validator