Theorem riin0

Description: Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015)

	Ref	Expression
Assertion	riin0	$$⊢X=\varnothing \to A\cap \bigcap _{x\in X}S=A$$

Proof

Step	Hyp	Ref	Expression
1		iineq1	$$⊢X=\varnothing \to \bigcap _{x\in X}S=\bigcap _{x\in \varnothing }S$$
2	1	ineq2d	$$⊢X=\varnothing \to A\cap \bigcap _{x\in X}S=A\cap \bigcap _{x\in \varnothing }S$$
3		0iin	$$⊢\bigcap _{x\in \varnothing }S=\mathrm{V}$$
4	3	ineq2i	$$⊢A\cap \bigcap _{x\in \varnothing }S=A\cap \mathrm{V}$$
5		inv1	$$⊢A\cap \mathrm{V}=A$$
6	4 5	eqtri	$$⊢A\cap \bigcap _{x\in \varnothing }S=A$$
7	2 6	eqtrdi	$$⊢X=\varnothing \to A\cap \bigcap _{x\in X}S=A$$