Metamath Proof Explorer


Theorem unabs

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

Ref Expression
Assertion unabs A A B = A

Proof

Step Hyp Ref Expression
1 inss1 A B A
2 ssequn2 A B A A A B = A
3 1 2 mpbi A A B = A