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 i^i C ) = (/) -> ( A u. ( B \ C ) ) = ( ( A u. B ) \ C ) )

Proof

Step Hyp Ref Expression
1 pm2.621 
 |-  ( ( x e. A -> -. x e. C ) -> ( ( x e. A \/ -. x e. C ) -> -. x e. C ) )
2 olc 
 |-  ( -. x e. C -> ( x e. A \/ -. x e. C ) )
3 1 2 impbid1 
 |-  ( ( x e. A -> -. x e. C ) -> ( ( x e. A \/ -. x e. C ) <-> -. x e. C ) )
4 3 anbi2d 
 |-  ( ( x e. A -> -. x e. C ) -> ( ( ( x e. A \/ x e. B ) /\ ( x e. A \/ -. x e. C ) ) <-> ( ( x e. A \/ x e. B ) /\ -. x e. C ) ) )
5 eldif 
 |-  ( x e. ( B \ C ) <-> ( x e. B /\ -. x e. C ) )
6 5 orbi2i 
 |-  ( ( x e. A \/ x e. ( B \ C ) ) <-> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
7 ordi 
 |-  ( ( x e. A \/ ( x e. B /\ -. x e. C ) ) <-> ( ( x e. A \/ x e. B ) /\ ( x e. A \/ -. x e. C ) ) )
8 6 7 bitri 
 |-  ( ( x e. A \/ x e. ( B \ C ) ) <-> ( ( x e. A \/ x e. B ) /\ ( x e. A \/ -. x e. C ) ) )
9 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
10 9 anbi1i 
 |-  ( ( x e. ( A u. B ) /\ -. x e. C ) <-> ( ( x e. A \/ x e. B ) /\ -. x e. C ) )
11 4 8 10 3bitr4g 
 |-  ( ( x e. A -> -. x e. C ) -> ( ( x e. A \/ x e. ( B \ C ) ) <-> ( x e. ( A u. B ) /\ -. x e. C ) ) )
12 elun 
 |-  ( x e. ( A u. ( B \ C ) ) <-> ( x e. A \/ x e. ( B \ C ) ) )
13 eldif 
 |-  ( x e. ( ( A u. B ) \ C ) <-> ( x e. ( A u. B ) /\ -. x e. C ) )
14 11 12 13 3bitr4g 
 |-  ( ( x e. A -> -. x e. C ) -> ( x e. ( A u. ( B \ C ) ) <-> x e. ( ( A u. B ) \ C ) ) )
15 14 alimi 
 |-  ( A. x ( x e. A -> -. x e. C ) -> A. x ( x e. ( A u. ( B \ C ) ) <-> x e. ( ( A u. B ) \ C ) ) )
16 disj1 
 |-  ( ( A i^i C ) = (/) <-> A. x ( x e. A -> -. x e. C ) )
17 dfcleq 
 |-  ( ( A u. ( B \ C ) ) = ( ( A u. B ) \ C ) <-> A. x ( x e. ( A u. ( B \ C ) ) <-> x e. ( ( A u. B ) \ C ) ) )
18 15 16 17 3imtr4i 
 |-  ( ( A i^i C ) = (/) -> ( A u. ( B \ C ) ) = ( ( A u. B ) \ C ) )