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.

Step	Hyp	Ref	Expression
1		raleq 2907	. . 3 |- ( A = B -> ( A. y e. A x e. y <-> A. y e. B x e. y ) )
2	1	abbidv 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 }
5	2, 3, 4	3eqtr4g 2490	1 |- ( A = B -> |^| A = |^| B )

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