Metamath Proof Explorer


Theorem eqrelrd2

Description: A version of eqrelrdv2 with explicit nonfree declarations. (Contributed by Thierry Arnoux, 28-Aug-2017)

Ref Expression
Hypotheses eqrelrd2.1 x φ
eqrelrd2.2 y φ
eqrelrd2.3 _ x A
eqrelrd2.4 _ y A
eqrelrd2.5 _ x B
eqrelrd2.6 _ y B
eqrelrd2.7 φ x y A x y B
Assertion eqrelrd2 Rel A Rel B φ A = B

Proof

Step Hyp Ref Expression
1 eqrelrd2.1 x φ
2 eqrelrd2.2 y φ
3 eqrelrd2.3 _ x A
4 eqrelrd2.4 _ y A
5 eqrelrd2.5 _ x B
6 eqrelrd2.6 _ y B
7 eqrelrd2.7 φ x y A x y B
8 2 7 alrimi φ y x y A x y B
9 1 8 alrimi φ x y x y A x y B
10 9 adantl Rel A Rel B φ x y x y A x y B
11 1 2 3 4 5 6 ssrelf Rel A A B x y x y A x y B
12 1 2 5 6 3 4 ssrelf Rel B B A x y x y B x y A
13 11 12 bi2anan9 Rel A Rel B A B B A x y x y A x y B x y x y B x y A
14 eqss A = B A B B A
15 2albiim x y x y A x y B x y x y A x y B x y x y B x y A
16 13 14 15 3bitr4g Rel A Rel B A = B x y x y A x y B
17 16 adantr Rel A Rel B φ A = B x y x y A x y B
18 10 17 mpbird Rel A Rel B φ A = B