Metamath Proof Explorer


Theorem eqrel2

Description: Equality of relations. (Contributed by Peter Mazsa, 8-Mar-2019)

Ref Expression
Assertion eqrel2 Rel A Rel B A = B x y x A y x B y

Proof

Step Hyp Ref Expression
1 ssrel3 Rel A A B x y x A y x B y
2 ssrel3 Rel B B A x y x B y x A y
3 1 2 bi2anan9 Rel A Rel B A B B A x y x A y x B y x y x B y x A y
4 eqss A = B A B B A
5 2albiim x y x A y x B y x y x A y x B y x y x B y x A y
6 3 4 5 3bitr4g Rel A Rel B A = B x y x A y x B y