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 )