Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
General Set Theory
Set relations and operations - misc additions
undifr
Next ⟩
indifundif
Metamath Proof Explorer
Ascii
Unicode
Theorem
undifr
Description:
Union of complementary parts into whole.
(Contributed by
Thierry Arnoux
, 21-Nov-2023)
Ref
Expression
Assertion
undifr
⊢
A
⊆
B
↔
B
∖
A
∪
A
=
B
Proof
Step
Hyp
Ref
Expression
1
undif
⊢
A
⊆
B
↔
A
∪
B
∖
A
=
B
2
uncom
⊢
A
∪
B
∖
A
=
B
∖
A
∪
A
3
2
eqeq1i
⊢
A
∪
B
∖
A
=
B
↔
B
∖
A
∪
A
=
B
4
1
3
bitri
⊢
A
⊆
B
↔
B
∖
A
∪
A
=
B