Theorem unabs

Description: Absorption law for union. (Contributed by NM, 16-Apr-2006)

	Ref	Expression
Assertion	unabs	|- ( A u. ( A i^i B ) ) = A

Proof

Step	Hyp	Ref	Expression
1		inss1	|- ( A i^i B ) C_ A
2		ssequn2	|- ( ( A i^i B ) C_ A <-> ( A u. ( A i^i B ) ) = A )
3	1 2	mpbi	|- ( A u. ( A i^i B ) ) = A