Theorem iinvdif

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

	Ref	Expression
Assertion	iinvdif	$$⊢\bigcap _{x\in A}\left(\mathrm{V}\setminus B\right)=\mathrm{V}\setminus \bigcup _{x\in A}B$$

Proof

Step	Hyp	Ref	Expression
1		dif0	$$⊢\mathrm{V}\setminus \varnothing =\mathrm{V}$$
2		0iun	$$⊢\bigcup _{x\in \varnothing }B=\varnothing$$
3	2	difeq2i	$$⊢\mathrm{V}\setminus \bigcup _{x\in \varnothing }B=\mathrm{V}\setminus \varnothing$$
4		0iin	$$⊢\bigcap _{x\in \varnothing }\left(\mathrm{V}\setminus B\right)=\mathrm{V}$$
5	1 3 4	3eqtr4ri	$$⊢\bigcap _{x\in \varnothing }\left(\mathrm{V}\setminus B\right)=\mathrm{V}\setminus \bigcup _{x\in \varnothing }B$$
6		iineq1	$$⊢A=\varnothing \to \bigcap _{x\in A}\left(\mathrm{V}\setminus B\right)=\bigcap _{x\in \varnothing }\left(\mathrm{V}\setminus B\right)$$
7		iuneq1	$$⊢A=\varnothing \to \bigcup _{x\in A}B=\bigcup _{x\in \varnothing }B$$
8	7	difeq2d	$$⊢A=\varnothing \to \mathrm{V}\setminus \bigcup _{x\in A}B=\mathrm{V}\setminus \bigcup _{x\in \varnothing }B$$
9	5 6 8	3eqtr4a	$$⊢A=\varnothing \to \bigcap _{x\in A}\left(\mathrm{V}\setminus B\right)=\mathrm{V}\setminus \bigcup _{x\in A}B$$
10		iindif2	$$⊢A\ne \varnothing \to \bigcap _{x\in A}\left(\mathrm{V}\setminus B\right)=\mathrm{V}\setminus \bigcup _{x\in A}B$$
11	9 10	pm2.61ine	$$⊢\bigcap _{x\in A}\left(\mathrm{V}\setminus B\right)=\mathrm{V}\setminus \bigcup _{x\in A}B$$