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	|- ( E. x e. A Rel B -> Rel |^|_ x e. A B )

Proof

Step	Hyp	Ref	Expression
1		iinss	|- ( E. x e. A B C_ ( _V X. _V ) -> |^|_ x e. A B C_ ( _V X. _V ) )
2		df-rel	|- ( Rel B <-> B C_ ( _V X. _V ) )
3	2	rexbii	|- ( E. x e. A Rel B <-> E. x e. A B C_ ( _V X. _V ) )
4		df-rel	|- ( Rel |^|_ x e. A B <-> |^|_ x e. A B C_ ( _V X. _V ) )
5	1 3 4	3imtr4i	|- ( E. x e. A Rel B -> Rel |^|_ x e. A B )