Metamath Proof Explorer


Theorem relin2

Description: The intersection with a relation is a relation. (Contributed by NM, 17-Jan-2006)

Ref Expression
Assertion relin2 ( Rel 𝐵 → Rel ( 𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 inss2 ( 𝐴𝐵 ) ⊆ 𝐵
2 relss ( ( 𝐴𝐵 ) ⊆ 𝐵 → ( Rel 𝐵 → Rel ( 𝐴𝐵 ) ) )
3 1 2 ax-mp ( Rel 𝐵 → Rel ( 𝐴𝐵 ) )