Theorem inteq 4229

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 3003	. . 3 |- ( A = B -> ( A. y e. A x e. y <-> A. y e. B x e. y ) )
2	1	abbidv 2538	. 2 |- ( A = B -> { x | A. y e. A x e. y } = { x | A. y e. B x e. y } )
3		dfint2 4228	. 2 |- |^| A = { x | A. y e. A x e. y }
4		dfint2 4228	. 2 |- |^| B = { x | A. y e. B x e. y }
5	2, 3, 4	3eqtr4g 2468	1 |- ( A = B -> |^| A = |^| B )

Syntax hints:   -> wi 4   = wceq 1405   {cab 2387   A.wral 2753   |^|cint 4226

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2758  df-int 4227

This theorem is referenced by:  inteqi  4230  inteqd  4231  unissint  4251  uniintsn  4264  rint0  4267  intex  4549  intnex  4550  elreldm  5047  elxp5  6728  1stval2  6800  oev2  7209  fundmen  7626  xpsnen  7638  fiint  7830  elfir  7908  inelfi  7911  fiin  7915  cardmin2  8410  isfin2-2  8730  incexclem  13797  mreintcl  15207  ismred2  15215  fiinopn  19700  cmpfii  20200  ptbasfi  20372  fbssint  20629  shintcl  26648  chintcl  26650  inelpisys  28588  rankeq1o  30496  neificl  31508  heibor1lem  31567  elrfi  34968  elrfirn  34969