Metamath Proof Explorer

Theorem difunieq

Description: The difference of unions is a subset of the union of the difference. (Contributed by ML, 29-Mar-2021)

Ref Expression
Assertion difunieq 
|- ( U. A \ U. B ) C_ U. ( A \ B )

Proof

Step Hyp Ref Expression
1 eluni 
 |-  ( x e. U. A <-> E. y ( x e. y /\ y e. A ) )
2 eluni 
 |-  ( x e. U. B <-> E. y ( x e. y /\ y e. B ) )
3 2 notbii 
 |-  ( -. x e. U. B <-> -. E. y ( x e. y /\ y e. B ) )
4 alinexa 
 |-  ( A. y ( x e. y -> -. y e. B ) <-> -. E. y ( x e. y /\ y e. B ) )
5 nfa1 
 |-  F/ y A. y ( x e. y -> -. y e. B )
6 sp 
 |-  ( A. y ( x e. y -> -. y e. B ) -> ( x e. y -> -. y e. B ) )
7 6 adantrd 
 |-  ( A. y ( x e. y -> -. y e. B ) -> ( ( x e. y /\ y e. A ) -> -. y e. B ) )
8 7 ancld 
 |-  ( A. y ( x e. y -> -. y e. B ) -> ( ( x e. y /\ y e. A ) -> ( ( x e. y /\ y e. A ) /\ -. y e. B ) ) )
9 anass 
 |-  ( ( ( x e. y /\ y e. A ) /\ -. y e. B ) <-> ( x e. y /\ ( y e. A /\ -. y e. B ) ) )
10 8 9 imbitrdi 
 |-  ( A. y ( x e. y -> -. y e. B ) -> ( ( x e. y /\ y e. A ) -> ( x e. y /\ ( y e. A /\ -. y e. B ) ) ) )
11 5 10 eximd 
 |-  ( A. y ( x e. y -> -. y e. B ) -> ( E. y ( x e. y /\ y e. A ) -> E. y ( x e. y /\ ( y e. A /\ -. y e. B ) ) ) )
12 4 11 sylbir 
 |-  ( -. E. y ( x e. y /\ y e. B ) -> ( E. y ( x e. y /\ y e. A ) -> E. y ( x e. y /\ ( y e. A /\ -. y e. B ) ) ) )
13 12 impcom 
 |-  ( ( E. y ( x e. y /\ y e. A ) /\ -. E. y ( x e. y /\ y e. B ) ) -> E. y ( x e. y /\ ( y e. A /\ -. y e. B ) ) )
14 1 3 13 syl2anb 
 |-  ( ( x e. U. A /\ -. x e. U. B ) -> E. y ( x e. y /\ ( y e. A /\ -. y e. B ) ) )
15 eldif 
 |-  ( x e. ( U. A \ U. B ) <-> ( x e. U. A /\ -. x e. U. B ) )
16 eluni 
 |-  ( x e. U. ( A \ B ) <-> E. y ( x e. y /\ y e. ( A \ B ) ) )
17 eldif 
 |-  ( y e. ( A \ B ) <-> ( y e. A /\ -. y e. B ) )
18 17 anbi2i 
 |-  ( ( x e. y /\ y e. ( A \ B ) ) <-> ( x e. y /\ ( y e. A /\ -. y e. B ) ) )
19 18 exbii 
 |-  ( E. y ( x e. y /\ y e. ( A \ B ) ) <-> E. y ( x e. y /\ ( y e. A /\ -. y e. B ) ) )
20 16 19 bitri 
 |-  ( x e. U. ( A \ B ) <-> E. y ( x e. y /\ ( y e. A /\ -. y e. B ) ) )
21 14 15 20 3imtr4i 
 |-  ( x e. ( U. A \ U. B ) -> x e. U. ( A \ B ) )
22 21 ssriv 
 |-  ( U. A \ U. B ) C_ U. ( A \ B )