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

Metamath Proof Explorer

Theorem undifr

Description: Union of complementary parts into whole. (Contributed by Thierry Arnoux, 21-Nov-2023) (Proof shortened by SN, 11-Mar-2025)

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

Proof

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