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

Metamath Proof Explorer

Theorem rint0

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

		Ref	Expression
	Assertion	rint0	$⊢ X = \emptyset \to A \cap ⋂ X = A$

Step	Hyp	Ref	Expression
1		inteq	$⊢ X = \emptyset \to ⋂ X = ⋂ \emptyset$
2	1	ineq2d	$⊢ X = \emptyset \to A \cap ⋂ X = A \cap ⋂ \emptyset$
3		int0	$⊢ ⋂ \emptyset = V$
4	3	ineq2i	$⊢ A \cap ⋂ \emptyset = A \cap V$
5		inv1	$⊢ A \cap V = A$
6	4 5	eqtri	$⊢ A \cap ⋂ \emptyset = A$
7	2 6	eqtrdi	$⊢ X = \emptyset \to A \cap ⋂ X = A$