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

Metamath Proof Explorer

Theorem relint

Description: The intersection of a class is a relation if at least one member is a relation. (Contributed by NM, 8-Mar-2014)

		Ref	Expression
	Assertion	relint	$⊢ \exists x \in A Rel x \to Rel ⋂ A$

Step	Hyp	Ref	Expression
1		reliin	$⊢ \exists x \in A Rel x \to Rel ⋂_{x \in A} x$
2		intiin	$⊢ ⋂ A = ⋂_{x \in A} x$
3	2	releqi	$⊢ Rel ⋂ A \leftrightarrow Rel ⋂_{x \in A} x$
4	1 3	sylibr	$⊢ \exists x \in A Rel x \to Rel ⋂ A$