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

Proof

Step	Hyp	Ref	Expression
1		reliin	|- ( E. x e. A Rel x -> Rel |^|_ x e. A x )
2		intiin	|- |^| A = |^|_ x e. A x
3	2	releqi	|- ( Rel |^| A <-> Rel |^|_ x e. A x )
4	1 3	sylibr	|- ( E. x e. A Rel x -> Rel |^| A )