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

Theorem inteq 4119
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 2907 . . 3  |-  ( A  =  B  ->  ( A. y  e.  A  x  e.  y  <->  A. y  e.  B  x  e.  y ) )
21abbidv 2547 . 2  |-  ( A  =  B  ->  { x  |  A. y  e.  A  x  e.  y }  =  { x  |  A. y  e.  B  x  e.  y } )
3 dfint2 4118 . 2  |-  |^| A  =  { x  |  A. y  e.  A  x  e.  y }
4 dfint2 4118 . 2  |-  |^| B  =  { x  |  A. y  e.  B  x  e.  y }
52, 3, 43eqtr4g 2490 1  |-  ( A  =  B  ->  |^| A  =  |^| B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362   {cab 2419   A.wral 2705   |^|cint 4116
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-int 4117
This theorem is referenced by:  inteqi  4120  inteqd  4121  unissint  4140  uniintsn  4153  rint0  4156  intex  4436  intnex  4437  elreldm  5051  elxp5  6512  1stval2  6583  oev2  6951  fundmen  7371  xpsnen  7383  fiint  7576  elfir  7653  inelfi  7656  fiin  7660  cardmin2  8156  isfin2-2  8476  incexclem  13281  xpnnenOLD  13474  mreintcl  14515  ismred2  14523  fiinopn  18355  cmpfii  18853  ptbasfi  18995  fbssint  19252  shintcl  24555  chintcl  24557  rankeq1o  28055  neificl  28490  heibor1lem  28549  elrfi  28872  elrfirn  28873
  Copyright terms: Public domain W3C validator