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 i^i ( A u. B ) ) = A

Proof

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