Theorem inteq 4478

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.

Step	Hyp	Ref	Expression
1		raleq 3138	. . 3 |- ( A = B -> ( A. y e. A x e. y <-> A. y e. B x e. y ) )
2	1	abbidv 2741	. 2 |- ( A = B -> { x | A. y e. A x e. y } = { x | A. y e. B x e. y } )
3		dfint2 4477	. 2 |- |^| A = { x | A. y e. A x e. y }
4		dfint2 4477	. 2 |- |^| B = { x | A. y e. B x e. y }
5	2, 3, 4	3eqtr4g 2681	1 |- ( A = B -> |^| A = |^| B )

Syntax hints:   -> wi 4   = wceq 1483   {cab 2608   A.wral 2912   |^|cint 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-int 4476

This theorem is referenced by:  inteqi  4479  inteqd  4480  unissint  4501  uniintsn  4514  rint0  4517  intex  4820  intnex  4821  elreldm  5350  elxp5  7111  1stval2  7185  oev2  7603  fundmen  8030  xpsnen  8044  fiint  8237  elfir  8321  inelfi  8324  fiin  8328  cardmin2  8824  isfin2-2  9141  incexclem  14568  mreintcl  16255  ismred2  16263  fiinopn  20706  cmpfii  21212  ptbasfi  21384  fbssint  21642  shintcl  28189  chintcl  28191  inelpisys  30217  rankeq1o  32278  bj-0int  33055  bj-ismoored  33062  bj-snmoore  33068  neificl  33549  heibor1lem  33608  elrfi  37257  elrfirn  37258