Theorem inteq 4238

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 3021	. . 3 |- ( A = B -> ( A. y e. A x e. y <-> A. y e. B x e. y ) )
2	1	abbidv 2590	. 2 |- ( A = B -> { x | A. y e. A x e. y } = { x | A. y e. B x e. y } )
3		dfint2 4237	. 2 |- |^| A = { x | A. y e. A x e. y }
4		dfint2 4237	. 2 |- |^| B = { x | A. y e. B x e. y }
5	2, 3, 4	3eqtr4g 2520	1 |- ( A = B -> |^| A = |^| B )

Syntax hints:   -> wi 4   = wceq 1370   {cab 2439   A.wral 2798   |^|cint 4235

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2803  df-int 4236

This theorem is referenced by:  inteqi  4239  inteqd  4240  unissint  4259  uniintsn  4272  rint0  4275  intex  4555  intnex  4556  elreldm  5171  elxp5  6632  1stval2  6703  oev2  7072  fundmen  7492  xpsnen  7504  fiint  7698  elfir  7775  inelfi  7778  fiin  7782  cardmin2  8278  isfin2-2  8598  incexclem  13416  xpnnenOLD  13609  mreintcl  14651  ismred2  14659  fiinopn  18645  cmpfii  19143  ptbasfi  19285  fbssint  19542  shintcl  24884  chintcl  24886  rankeq1o  28352  neificl  28796  heibor1lem  28855  elrfi  29177  elrfirn  29178