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

Theorem inteq 3867
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 2738 . . 3  |-  ( A  =  B  ->  ( A. y  e.  A  x  e.  y  <->  A. y  e.  B  x  e.  y ) )
21abbidv 2399 . 2  |-  ( A  =  B  ->  { x  |  A. y  e.  A  x  e.  y }  =  { x  |  A. y  e.  B  x  e.  y } )
3 dfint2 3866 . 2  |-  |^| A  =  { x  |  A. y  e.  A  x  e.  y }
4 dfint2 3866 . 2  |-  |^| B  =  { x  |  A. y  e.  B  x  e.  y }
52, 3, 43eqtr4g 2342 1  |-  ( A  =  B  ->  |^| A  =  |^| B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625    e. wcel 1686   {cab 2271   A.wral 2545   |^|cint 3864
This theorem is referenced by:  inteqi  3868  inteqd  3869  unissint  3888  uniintsn  3901  rint0  3904  intex  4169  intnex  4170  elreldm  4905  elxp5  5163  1stval2  6139  oev2  6524  fundmen  6936  xpsnen  6948  fiint  7135  elfir  7171  fiin  7177  cardmin2  7633  isfin2-2  7947  incexclem  12297  incexc  12298  xpnnenOLD  12490  mreintcl  13499  ismred2  13507  fiinopn  16649  cmpfii  17138  ptbasfi  17278  fbssint  17535  shintcl  21911  chintcl  21913  rankeq1o  24803  isconcl2b  26109  neificl  26478  heibor1lem  26544  elrfi  26780  elrfirn  26781
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ral 2550  df-int 3865
  Copyright terms: Public domain W3C validator