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 C = A B C = A B C

Proof

Step Hyp Ref Expression
1 pm2.621 x A ¬ x C x A ¬ x C ¬ x C
2 olc ¬ x C x A ¬ x C
3 1 2 impbid1 x A ¬ x C x A ¬ x C ¬ x C
4 3 anbi2d x A ¬ x C x A x B x A ¬ x C x A x B ¬ x C
5 eldif x B C x B ¬ x C
6 5 orbi2i x A x B C x A x B ¬ x C
7 ordi x A x B ¬ x C x A x B x A ¬ x C
8 6 7 bitri x A x B C x A x B x A ¬ x C
9 elun x A B x A x B
10 9 anbi1i x A B ¬ x C x A x B ¬ x C
11 4 8 10 3bitr4g x A ¬ x C x A x B C x A B ¬ x C
12 elun x A B C x A x B C
13 eldif x A B C x A B ¬ x C
14 11 12 13 3bitr4g x A ¬ x C x A B C x A B C
15 14 alimi x x A ¬ x C x x A B C x A B C
16 disj1 A C = x x A ¬ x C
17 dfcleq A B C = A B C x x A B C x A B C
18 15 16 17 3imtr4i A C = A B C = A B C