Metamath Proof Explorer


Theorem ssbr

Description: Implication from a subclass relationship of binary relations. (Contributed by Peter Mazsa, 11-Nov-2019)

Ref Expression
Assertion ssbr ABCADCBD

Proof

Step Hyp Ref Expression
1 id ABAB
2 1 ssbrd ABCADCBD