Theorem inabs

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

	Ref	Expression
Assertion	inabs	⊢ ( 𝐴 ∩ ( 𝐴 ∪ 𝐵 ) ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
2		dfss2	⊢ ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝐴 ∩ ( 𝐴 ∪ 𝐵 ) ) = 𝐴 )
3	1 2	mpbi	⊢ ( 𝐴 ∩ ( 𝐴 ∪ 𝐵 ) ) = 𝐴