Theorem inteq 4126

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 2912	. . 3 |- ( A = B -> ( A. y e. A x e. y <-> A. y e. B x e. y ) )
2	1	abbidv 2552	. 2 |- ( A = B -> { x | A. y e. A x e. y } = { x | A. y e. B x e. y } )
3		dfint2 4125	. 2 |- |^| A = { x | A. y e. A x e. y }
4		dfint2 4125	. 2 |- |^| B = { x | A. y e. B x e. y }
5	2, 3, 4	3eqtr4g 2495	1 |- ( A = B -> |^| A = |^| B )

Syntax hints:   -> wi 4   = wceq 1369   {cab 2424   A.wral 2710   |^|cint 4123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-int 4124

This theorem is referenced by:  inteqi  4127  inteqd  4128  unissint  4147  uniintsn  4160  rint0  4163  intex  4443  intnex  4444  elreldm  5059  elxp5  6518  1stval2  6589  oev2  6955  fundmen  7375  xpsnen  7387  fiint  7580  elfir  7657  inelfi  7660  fiin  7664  cardmin2  8160  isfin2-2  8480  incexclem  13291  xpnnenOLD  13484  mreintcl  14525  ismred2  14533  fiinopn  18494  cmpfii  18992  ptbasfi  19134  fbssint  19391  shintcl  24701  chintcl  24703  rankeq1o  28178  neificl  28620  heibor1lem  28679  elrfi  29001  elrfirn  29002