This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem riin0

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

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

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