# Metamath Proof Explorer

## Theorem uneqdifeq

Description: Two ways to say that A and B partition C (when A and B don't overlap and A is a part of C ). (Contributed by FL, 17-Nov-2008) (Proof shortened by JJ, 14-Jul-2021)

Ref Expression
Assertion uneqdifeq ${⊢}\left({A}\subseteq {C}\wedge {A}\cap {B}=\varnothing \right)\to \left({A}\cup {B}={C}↔{C}\setminus {A}={B}\right)$

### Proof

Step Hyp Ref Expression
1 uncom ${⊢}{B}\cup {A}={A}\cup {B}$
2 eqtr ${⊢}\left({B}\cup {A}={A}\cup {B}\wedge {A}\cup {B}={C}\right)\to {B}\cup {A}={C}$
3 2 eqcomd ${⊢}\left({B}\cup {A}={A}\cup {B}\wedge {A}\cup {B}={C}\right)\to {C}={B}\cup {A}$
4 difeq1 ${⊢}{C}={B}\cup {A}\to {C}\setminus {A}=\left({B}\cup {A}\right)\setminus {A}$
5 difun2 ${⊢}\left({B}\cup {A}\right)\setminus {A}={B}\setminus {A}$
6 eqtr ${⊢}\left({C}\setminus {A}=\left({B}\cup {A}\right)\setminus {A}\wedge \left({B}\cup {A}\right)\setminus {A}={B}\setminus {A}\right)\to {C}\setminus {A}={B}\setminus {A}$
7 incom ${⊢}{A}\cap {B}={B}\cap {A}$
8 7 eqeq1i ${⊢}{A}\cap {B}=\varnothing ↔{B}\cap {A}=\varnothing$
9 disj3 ${⊢}{B}\cap {A}=\varnothing ↔{B}={B}\setminus {A}$
10 8 9 bitri ${⊢}{A}\cap {B}=\varnothing ↔{B}={B}\setminus {A}$
11 eqtr ${⊢}\left({C}\setminus {A}={B}\setminus {A}\wedge {B}\setminus {A}={B}\right)\to {C}\setminus {A}={B}$
12 11 expcom ${⊢}{B}\setminus {A}={B}\to \left({C}\setminus {A}={B}\setminus {A}\to {C}\setminus {A}={B}\right)$
13 12 eqcoms ${⊢}{B}={B}\setminus {A}\to \left({C}\setminus {A}={B}\setminus {A}\to {C}\setminus {A}={B}\right)$
14 10 13 sylbi ${⊢}{A}\cap {B}=\varnothing \to \left({C}\setminus {A}={B}\setminus {A}\to {C}\setminus {A}={B}\right)$
15 6 14 syl5com ${⊢}\left({C}\setminus {A}=\left({B}\cup {A}\right)\setminus {A}\wedge \left({B}\cup {A}\right)\setminus {A}={B}\setminus {A}\right)\to \left({A}\cap {B}=\varnothing \to {C}\setminus {A}={B}\right)$
16 4 5 15 sylancl ${⊢}{C}={B}\cup {A}\to \left({A}\cap {B}=\varnothing \to {C}\setminus {A}={B}\right)$
17 3 16 syl ${⊢}\left({B}\cup {A}={A}\cup {B}\wedge {A}\cup {B}={C}\right)\to \left({A}\cap {B}=\varnothing \to {C}\setminus {A}={B}\right)$
18 1 17 mpan ${⊢}{A}\cup {B}={C}\to \left({A}\cap {B}=\varnothing \to {C}\setminus {A}={B}\right)$
19 18 com12 ${⊢}{A}\cap {B}=\varnothing \to \left({A}\cup {B}={C}\to {C}\setminus {A}={B}\right)$
20 19 adantl ${⊢}\left({A}\subseteq {C}\wedge {A}\cap {B}=\varnothing \right)\to \left({A}\cup {B}={C}\to {C}\setminus {A}={B}\right)$
21 simpl ${⊢}\left({A}\subseteq {C}\wedge {C}\setminus {A}={B}\right)\to {A}\subseteq {C}$
22 difssd ${⊢}{C}\setminus {A}={B}\to {C}\setminus {A}\subseteq {C}$
23 sseq1 ${⊢}{C}\setminus {A}={B}\to \left({C}\setminus {A}\subseteq {C}↔{B}\subseteq {C}\right)$
24 22 23 mpbid ${⊢}{C}\setminus {A}={B}\to {B}\subseteq {C}$
25 24 adantl ${⊢}\left({A}\subseteq {C}\wedge {C}\setminus {A}={B}\right)\to {B}\subseteq {C}$
26 21 25 unssd ${⊢}\left({A}\subseteq {C}\wedge {C}\setminus {A}={B}\right)\to {A}\cup {B}\subseteq {C}$
27 eqimss ${⊢}{C}\setminus {A}={B}\to {C}\setminus {A}\subseteq {B}$
28 ssundif ${⊢}{C}\subseteq {A}\cup {B}↔{C}\setminus {A}\subseteq {B}$
29 27 28 sylibr ${⊢}{C}\setminus {A}={B}\to {C}\subseteq {A}\cup {B}$
30 29 adantl ${⊢}\left({A}\subseteq {C}\wedge {C}\setminus {A}={B}\right)\to {C}\subseteq {A}\cup {B}$
31 26 30 eqssd ${⊢}\left({A}\subseteq {C}\wedge {C}\setminus {A}={B}\right)\to {A}\cup {B}={C}$
32 31 ex ${⊢}{A}\subseteq {C}\to \left({C}\setminus {A}={B}\to {A}\cup {B}={C}\right)$
33 32 adantr ${⊢}\left({A}\subseteq {C}\wedge {A}\cap {B}=\varnothing \right)\to \left({C}\setminus {A}={B}\to {A}\cup {B}={C}\right)$
34 20 33 impbid ${⊢}\left({A}\subseteq {C}\wedge {A}\cap {B}=\varnothing \right)\to \left({A}\cup {B}={C}↔{C}\setminus {A}={B}\right)$