Theorem inteq 2533

Description: Equality law for intersection.

Assertion

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

Proof of Theorem inteq

Step	Hyp	Ref	Expression
1		raleq1 1785	. . 3 |- (A = B -> (A.y e. A x e. y <-> A.y e. B x e. y))
2	1	abbidv 1576	. 2 |- (A = B -> {x | A.y e. A x e. y} = {x | A.y e. B x e. y})
3		dfint2 2532	. 2 |- |^|A = {x | A.y e. A x e. y}
4		dfint2 2532	. 2 |- |^|B = {x | A.y e. B x e. y}
5	2, 3, 4	3eqtr4g 1530	1 |- (A = B -> |^|A = |^|B)

Syntax hints:   -> wi 3   = wceq 955   e. wcel 957  {cab 1463  A.wral 1644  |^|cint 2530

This theorem is referenced by:  inteqi 2534  inteqd 2535  intex 2726  intnex 2727  elreldm 3335  elxp5 3451  1stval2 4086  oev2 4159  fundmen 4422  xpsnen 4428  mapunen 4495  fiint 4547  abfii3 4550  abfii4 4551  xpnnen 7477  subbas 7623  subbas2 7624  shintclt 9282  chintclt 9284  infi1 10440  fine 10441  abfi 10442  fiiu 10443  ficli 10461  fiiu2 10471  fipfil2 10533  efilcp 10539  filint2 10540  infi 10542  efilcp2 10544  cnfilca 10545

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1648  df-int 2531

Copyright terms: Public domain