Theorem iinvdif

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

	Ref	Expression
Assertion	iinvdif	⊢ ∩ 𝑥 ∈ 𝐴 ( V ∖ 𝐵 ) = ( V ∖ ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dif0	⊢ ( V ∖ ∅ ) = V
2		0iun	⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅
3	2	difeq2i	⊢ ( V ∖ ∪ 𝑥 ∈ ∅ 𝐵 ) = ( V ∖ ∅ )
4		0iin	⊢ ∩ 𝑥 ∈ ∅ ( V ∖ 𝐵 ) = V
5	1 3 4	3eqtr4ri	⊢ ∩ 𝑥 ∈ ∅ ( V ∖ 𝐵 ) = ( V ∖ ∪ 𝑥 ∈ ∅ 𝐵 )
6		iineq1	⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 ( V ∖ 𝐵 ) = ∩ 𝑥 ∈ ∅ ( V ∖ 𝐵 ) )
7		iuneq1	⊢ ( 𝐴 = ∅ → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵 )
8	7	difeq2d	⊢ ( 𝐴 = ∅ → ( V ∖ ∪ 𝑥 ∈ 𝐴 𝐵 ) = ( V ∖ ∪ 𝑥 ∈ ∅ 𝐵 ) )
9	5 6 8	3eqtr4a	⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 ( V ∖ 𝐵 ) = ( V ∖ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
10		iindif2	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( V ∖ 𝐵 ) = ( V ∖ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
11	9 10	pm2.61ine	⊢ ∩ 𝑥 ∈ 𝐴 ( V ∖ 𝐵 ) = ( V ∖ ∪ 𝑥 ∈ 𝐴 𝐵 )