Theorem inteq

Description: Equality law for intersection. (Contributed by NM, 13-Sep-1999)

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

Proof

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