This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iundif2

Description: Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in Enderton p. 31. Use intiin to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004)

Ref Expression
Assertion iundif2 
|- U_ x e. A ( B \ C ) = ( B \ |^|_ x e. A C )

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( y e. ( B \ C ) <-> ( y e. B /\ -. y e. C ) )
2 1 rexbii 
 |-  ( E. x e. A y e. ( B \ C ) <-> E. x e. A ( y e. B /\ -. y e. C ) )
3 r19.42v 
 |-  ( E. x e. A ( y e. B /\ -. y e. C ) <-> ( y e. B /\ E. x e. A -. y e. C ) )
4 rexnal 
 |-  ( E. x e. A -. y e. C <-> -. A. x e. A y e. C )
5 eliin 
 |-  ( y e. _V -> ( y e. |^|_ x e. A C <-> A. x e. A y e. C ) )
6 5 elv 
 |-  ( y e. |^|_ x e. A C <-> A. x e. A y e. C )
7 4 6 xchbinxr 
 |-  ( E. x e. A -. y e. C <-> -. y e. |^|_ x e. A C )
8 7 anbi2i 
 |-  ( ( y e. B /\ E. x e. A -. y e. C ) <-> ( y e. B /\ -. y e. |^|_ x e. A C ) )
9 2 3 8 3bitri 
 |-  ( E. x e. A y e. ( B \ C ) <-> ( y e. B /\ -. y e. |^|_ x e. A C ) )
10 eliun 
 |-  ( y e. U_ x e. A ( B \ C ) <-> E. x e. A y e. ( B \ C ) )
11 eldif 
 |-  ( y e. ( B \ |^|_ x e. A C ) <-> ( y e. B /\ -. y e. |^|_ x e. A C ) )
12 9 10 11 3bitr4i 
 |-  ( y e. U_ x e. A ( B \ C ) <-> y e. ( B \ |^|_ x e. A C ) )
13 12 eqriv 
 |-  U_ x e. A ( B \ C ) = ( B \ |^|_ x e. A C )