Theorem unabs

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

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

Proof

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