Metamath Proof Explorer


Theorem ssrel3

Description: Subclass relation in another form when the subclass is a relation. (Contributed by Peter Mazsa, 16-Feb-2019)

Ref Expression
Assertion ssrel3 Rel A A B x y x A y x B y

Proof

Step Hyp Ref Expression
1 ssrel Rel A A B x y x y A x y B
2 df-br x A y x y A
3 df-br x B y x y B
4 2 3 imbi12i x A y x B y x y A x y B
5 4 2albii x y x A y x B y x y x y A x y B
6 1 5 bitr4di Rel A A B x y x A y x B y