Theorem iundif1

Description: Indexed union of class difference with the subtrahend held constant. (Contributed by Brendan Leahy, 6-Aug-2018)

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

Proof

Step	Hyp	Ref	Expression
1		r19.41v	|- ( E. x e. A ( y e. B /\ -. y e. C ) <-> ( E. x e. A y e. B /\ -. y e. C ) )
2		eldif	|- ( y e. ( B \ C ) <-> ( y e. B /\ -. y e. C ) )
3	2	rexbii	|- ( E. x e. A y e. ( B \ C ) <-> E. x e. A ( y e. B /\ -. y e. C ) )
4		eliun	|- ( y e. U_ x e. A B <-> E. x e. A y e. B )
5	4	anbi1i	|- ( ( y e. U_ x e. A B /\ -. y e. C ) <-> ( E. x e. A y e. B /\ -. y e. C ) )
6	1 3 5	3bitr4i	|- ( E. x e. A y e. ( B \ C ) <-> ( y e. U_ x e. A B /\ -. y e. C ) )
7		eliun	|- ( y e. U_ x e. A ( B \ C ) <-> E. x e. A y e. ( B \ C ) )
8		eldif	|- ( y e. ( U_ x e. A B \ C ) <-> ( y e. U_ x e. A B /\ -. y e. C ) )
9	6 7 8	3bitr4i	|- ( y e. U_ x e. A ( B \ C ) <-> y e. ( U_ x e. A B \ C ) )
10	9	eqriv	|- U_ x e. A ( B \ C ) = ( U_ x e. A B \ C )