Metamath Proof Explorer

Theorem relin1

Description: The intersection with a relation is a relation. (Contributed by NM, 16-Aug-1994)

Ref Expression
Assertion relin1 Rel A Rel A B


Step Hyp Ref Expression
1 inss1 A B A
2 relss A B A Rel A Rel A B
3 1 2 ax-mp Rel A Rel A B