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

Theorem inteq 4251
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 2999 . . 3  |-  ( A  =  B  ->  ( A. y  e.  A  x  e.  y  <->  A. y  e.  B  x  e.  y ) )
21abbidv 2580 . 2  |-  ( A  =  B  ->  { x  |  A. y  e.  A  x  e.  y }  =  { x  |  A. y  e.  B  x  e.  y } )
3 dfint2 4250 . 2  |-  |^| A  =  { x  |  A. y  e.  A  x  e.  y }
4 dfint2 4250 . 2  |-  |^| B  =  { x  |  A. y  e.  B  x  e.  y }
52, 3, 43eqtr4g 2521 1  |-  ( A  =  B  ->  |^| A  =  |^| B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455   {cab 2448   A.wral 2749   |^|cint 4248
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-int 4249
This theorem is referenced by:  inteqi  4252  inteqd  4253  unissint  4273  uniintsn  4286  rint0  4289  intex  4576  intnex  4577  elreldm  5081  elxp5  6770  1stval2  6842  oev2  7256  fundmen  7674  xpsnen  7687  fiint  7879  elfir  7960  inelfi  7963  fiin  7967  cardmin2  8463  isfin2-2  8780  incexclem  13949  mreintcl  15556  ismred2  15564  fiinopn  19986  cmpfii  20479  ptbasfi  20651  fbssint  20908  shintcl  27039  chintcl  27041  inelpisys  29027  rankeq1o  30988  neificl  32128  heibor1lem  32187  elrfi  35582  elrfirn  35583
  Copyright terms: Public domain W3C validator