This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inabs

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

		Ref	Expression
	Assertion	inabs	$⊢ A \cap (A \cup B) = A$

Step	Hyp	Ref	Expression
1		ssun1	$⊢ A \subseteq A \cup B$
2		dfss2	$⊢ A \subseteq A \cup B \leftrightarrow A \cap (A \cup B) = A$
3	1 2	mpbi	$⊢ A \cap (A \cup B) = A$