Theorem inteq 2540

Description: Equality law for intersection.

Assertion

Ref	Expression
inteq	|- (A = B -> |^|A = |^|B)

Proof of Theorem inteq

Step	Hyp	Ref	Expression
1		raleq1 1789	. . 3 |- (A = B -> (A.y e. A x e. y <-> A.y e. B x e. y))
2	1	abbidv 1580	. 2 |- (A = B -> {x | A.y e. A x e. y} = {x | A.y e. B x e. y})
3		dfint2 2539	. 2 |- |^|A = {x | A.y e. A x e. y}
4		dfint2 2539	. 2 |- |^|B = {x | A.y e. B x e. y}
5	2, 3, 4	3eqtr4g 1534	1 |- (A = B -> |^|A = |^|B)

Syntax hints:   -> wi 3   = wceq 958   e. wcel 960  {cab 1466  A.wral 1648  |^|cint 2537

This theorem is referenced by:  inteqi 2541  inteqd 2542  intex 2734  intnex 2735  elreldm 3344  elxp5 3460  1stval2 4095  oev2 4168  fundmen 4434  xpsnen 4441  mapunen 4508  fiint 4572  fiintOLD 4573  xpnnen 7500  shintclt 9289  chintclt 9291  infi1 10441  fine 10442  abfi 10443  fiiu 10444  ficli 10462  fiiu2 10473  fipfil2 10550  efilcp 10556  filint2 10557  infi 10559  efilcp2 10561  cnfilca 10562

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-int 2538

Copyright terms: Public domain