Theorem reliin

Description: An indexed intersection is a relation if at least one of the member of the indexed family is a relation. (Contributed by NM, 8-Mar-2014)

	Ref	Expression
Assertion	reliin	$$⊢\exists x\in A\mathrm{Rel}B\to \mathrm{Rel}\bigcap _{x\in A}B$$

Proof

Step	Hyp	Ref	Expression
1		iinss	$$⊢\exists x\in AB\subseteq \mathrm{V}\times \mathrm{V}\to \bigcap _{x\in A}B\subseteq \mathrm{V}\times \mathrm{V}$$
2		df-rel	$$⊢\mathrm{Rel}B\leftrightarrow B\subseteq \mathrm{V}\times \mathrm{V}$$
3	2	rexbii	$$⊢\exists x\in A\mathrm{Rel}B\leftrightarrow \exists x\in AB\subseteq \mathrm{V}\times \mathrm{V}$$
4		df-rel	$$⊢\mathrm{Rel}\bigcap _{x\in A}B\leftrightarrow \bigcap _{x\in A}B\subseteq \mathrm{V}\times \mathrm{V}$$
5	1 3 4	3imtr4i	$$⊢\exists x\in A\mathrm{Rel}B\to \mathrm{Rel}\bigcap _{x\in A}B$$