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 syl6ib
 |-  ( 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 )