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

Metamath Proof Explorer

Theorem undif

Description: Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998)

Ref Expression
Assertion undif ⊢ A ⊆ B ↔ A ∪ B ∖ A = B

Proof

Step Hyp Ref Expression
1 ssequn1 ⊢ A ⊆ B ↔ A ∪ B = B
2 undif2 ⊢ A ∪ B ∖ A = A ∪ B
3 2 eqeq1i ⊢ A ∪ B ∖ A = B ↔ A ∪ B = B
4 1 3 bitr4i ⊢ A ⊆ B ↔ A ∪ B ∖ A = B