Theorem iinvdif

Description: The indexed intersection of a complement. (Contributed by Gérard Lang, 5-Aug-2018)

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

Proof

Step	Hyp	Ref	Expression
1		dif0	|- ( _V \ (/) ) = _V
2		0iun	|- U_ x e. (/) B = (/)
3	2	difeq2i	|- ( _V \ U_ x e. (/) B ) = ( _V \ (/) )
4		0iin	|- |^|_ x e. (/) ( _V \ B ) = _V
5	1 3 4	3eqtr4ri	|- |^|_ x e. (/) ( _V \ B ) = ( _V \ U_ x e. (/) B )
6		iineq1	|- ( A = (/) -> |^|_ x e. A ( _V \ B ) = |^|_ x e. (/) ( _V \ B ) )
7		iuneq1	|- ( A = (/) -> U_ x e. A B = U_ x e. (/) B )
8	7	difeq2d	|- ( A = (/) -> ( _V \ U_ x e. A B ) = ( _V \ U_ x e. (/) B ) )
9	5 6 8	3eqtr4a	|- ( A = (/) -> |^|_ x e. A ( _V \ B ) = ( _V \ U_ x e. A B ) )
10		iindif2	|- ( A =/= (/) -> |^|_ x e. A ( _V \ B ) = ( _V \ U_ x e. A B ) )
11	9 10	pm2.61ine	|- |^|_ x e. A ( _V \ B ) = ( _V \ U_ x e. A B )