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	⊢ ( ∃ 𝑥 ∈ 𝐴 Rel 𝑥 → Rel ∩ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		reliin	⊢ ( ∃ 𝑥 ∈ 𝐴 Rel 𝑥 → Rel ∩ 𝑥 ∈ 𝐴 𝑥 )
2		intiin	⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥
3	2	releqi	⊢ ( Rel ∩ 𝐴 ↔ Rel ∩ 𝑥 ∈ 𝐴 𝑥 )
4	1 3	sylibr	⊢ ( ∃ 𝑥 ∈ 𝐴 Rel 𝑥 → Rel ∩ 𝐴 )