Theorem inteq 4251

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 2999	. . 3 |- ( A = B -> ( A. y e. A x e. y <-> A. y e. B x e. y ) )
2	1	abbidv 2580	. 2 |- ( A = B -> { x | A. y e. A x e. y } = { x | A. y e. B x e. y } )
3		dfint2 4250	. 2 |- |^| A = { x | A. y e. A x e. y }
4		dfint2 4250	. 2 |- |^| B = { x | A. y e. B x e. y }
5	2, 3, 4	3eqtr4g 2521	1 |- ( A = B -> |^| A = |^| B )

Syntax hints:   -> wi 4   = wceq 1455   {cab 2448   A.wral 2749   |^|cint 4248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-int 4249

This theorem is referenced by:  inteqi  4252  inteqd  4253  unissint  4273  uniintsn  4286  rint0  4289  intex  4576  intnex  4577  elreldm  5081  elxp5  6770  1stval2  6842  oev2  7256  fundmen  7674  xpsnen  7687  fiint  7879  elfir  7960  inelfi  7963  fiin  7967  cardmin2  8463  isfin2-2  8780  incexclem  13949  mreintcl  15556  ismred2  15564  fiinopn  19986  cmpfii  20479  ptbasfi  20651  fbssint  20908  shintcl  27039  chintcl  27041  inelpisys  29027  rankeq1o  30988  neificl  32128  heibor1lem  32187  elrfi  35582  elrfirn  35583