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\mathrm{Rel}x\to \mathrm{Rel}\bigcap A$$

Proof

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