Theorem inteq 4285

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 3058	. . 3 |- ( A = B -> ( A. y e. A x e. y <-> A. y e. B x e. y ) )
2	1	abbidv 2603	. 2 |- ( A = B -> { x | A. y e. A x e. y } = { x | A. y e. B x e. y } )
3		dfint2 4284	. 2 |- |^| A = { x | A. y e. A x e. y }
4		dfint2 4284	. 2 |- |^| B = { x | A. y e. B x e. y }
5	2, 3, 4	3eqtr4g 2533	1 |- ( A = B -> |^| A = |^| B )

Syntax hints:   -> wi 4   = wceq 1379   {cab 2452   A.wral 2814   |^|cint 4282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-int 4283

This theorem is referenced by:  inteqi  4286  inteqd  4287  unissint  4306  uniintsn  4319  rint0  4322  intex  4603  intnex  4604  elreldm  5225  elxp5  6726  1stval2  6798  oev2  7170  fundmen  7586  xpsnen  7598  fiint  7793  elfir  7871  inelfi  7874  fiin  7878  cardmin2  8375  isfin2-2  8695  incexclem  13607  xpnnenOLD  13800  mreintcl  14846  ismred2  14854  fiinopn  19177  cmpfii  19675  ptbasfi  19817  fbssint  20074  shintcl  25924  chintcl  25926  rankeq1o  29405  neificl  29849  heibor1lem  29908  elrfi  30230  elrfirn  30231