# Metamath Proof Explorer

## Theorem undif4

Description: Distribute union over difference. (Contributed by NM, 17-May-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011)

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

### Proof

Step Hyp Ref Expression
1 pm2.621 ${⊢}\left({x}\in {A}\to ¬{x}\in {C}\right)\to \left(\left({x}\in {A}\vee ¬{x}\in {C}\right)\to ¬{x}\in {C}\right)$
2 olc ${⊢}¬{x}\in {C}\to \left({x}\in {A}\vee ¬{x}\in {C}\right)$
3 1 2 impbid1 ${⊢}\left({x}\in {A}\to ¬{x}\in {C}\right)\to \left(\left({x}\in {A}\vee ¬{x}\in {C}\right)↔¬{x}\in {C}\right)$
4 3 anbi2d ${⊢}\left({x}\in {A}\to ¬{x}\in {C}\right)\to \left(\left(\left({x}\in {A}\vee {x}\in {B}\right)\wedge \left({x}\in {A}\vee ¬{x}\in {C}\right)\right)↔\left(\left({x}\in {A}\vee {x}\in {B}\right)\wedge ¬{x}\in {C}\right)\right)$
5 eldif ${⊢}{x}\in \left({B}\setminus {C}\right)↔\left({x}\in {B}\wedge ¬{x}\in {C}\right)$
6 5 orbi2i ${⊢}\left({x}\in {A}\vee {x}\in \left({B}\setminus {C}\right)\right)↔\left({x}\in {A}\vee \left({x}\in {B}\wedge ¬{x}\in {C}\right)\right)$
7 ordi ${⊢}\left({x}\in {A}\vee \left({x}\in {B}\wedge ¬{x}\in {C}\right)\right)↔\left(\left({x}\in {A}\vee {x}\in {B}\right)\wedge \left({x}\in {A}\vee ¬{x}\in {C}\right)\right)$
8 6 7 bitri ${⊢}\left({x}\in {A}\vee {x}\in \left({B}\setminus {C}\right)\right)↔\left(\left({x}\in {A}\vee {x}\in {B}\right)\wedge \left({x}\in {A}\vee ¬{x}\in {C}\right)\right)$
9 elun ${⊢}{x}\in \left({A}\cup {B}\right)↔\left({x}\in {A}\vee {x}\in {B}\right)$
10 9 anbi1i ${⊢}\left({x}\in \left({A}\cup {B}\right)\wedge ¬{x}\in {C}\right)↔\left(\left({x}\in {A}\vee {x}\in {B}\right)\wedge ¬{x}\in {C}\right)$
11 4 8 10 3bitr4g ${⊢}\left({x}\in {A}\to ¬{x}\in {C}\right)\to \left(\left({x}\in {A}\vee {x}\in \left({B}\setminus {C}\right)\right)↔\left({x}\in \left({A}\cup {B}\right)\wedge ¬{x}\in {C}\right)\right)$
12 elun ${⊢}{x}\in \left({A}\cup \left({B}\setminus {C}\right)\right)↔\left({x}\in {A}\vee {x}\in \left({B}\setminus {C}\right)\right)$
13 eldif ${⊢}{x}\in \left(\left({A}\cup {B}\right)\setminus {C}\right)↔\left({x}\in \left({A}\cup {B}\right)\wedge ¬{x}\in {C}\right)$
14 11 12 13 3bitr4g ${⊢}\left({x}\in {A}\to ¬{x}\in {C}\right)\to \left({x}\in \left({A}\cup \left({B}\setminus {C}\right)\right)↔{x}\in \left(\left({A}\cup {B}\right)\setminus {C}\right)\right)$
15 14 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to ¬{x}\in {C}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({A}\cup \left({B}\setminus {C}\right)\right)↔{x}\in \left(\left({A}\cup {B}\right)\setminus {C}\right)\right)$
16 disj1 ${⊢}{A}\cap {C}=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to ¬{x}\in {C}\right)$
17 dfcleq ${⊢}{A}\cup \left({B}\setminus {C}\right)=\left({A}\cup {B}\right)\setminus {C}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({A}\cup \left({B}\setminus {C}\right)\right)↔{x}\in \left(\left({A}\cup {B}\right)\setminus {C}\right)\right)$
18 15 16 17 3imtr4i ${⊢}{A}\cap {C}=\varnothing \to {A}\cup \left({B}\setminus {C}\right)=\left({A}\cup {B}\right)\setminus {C}$