Theorem rint0

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

	Ref	Expression
Assertion	rint0	$$⊢X=\varnothing \to A\cap \bigcap X=A$$

Proof

Step	Hyp	Ref	Expression
1		inteq	$$⊢X=\varnothing \to \bigcap X=\bigcap \varnothing$$
2	1	ineq2d	$$⊢X=\varnothing \to A\cap \bigcap X=A\cap \bigcap \varnothing$$
3		int0	$$⊢\bigcap \varnothing =\mathrm{V}$$
4	3	ineq2i	$$⊢A\cap \bigcap \varnothing =A\cap \mathrm{V}$$
5		inv1	$$⊢A\cap \mathrm{V}=A$$
6	4 5	eqtri	$$⊢A\cap \bigcap \varnothing =A$$
7	2 6	eqtrdi	$$⊢X=\varnothing \to A\cap \bigcap X=A$$