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
|- F/ x ph
eqrelrd2.2
|- F/ y ph
eqrelrd2.3
|- F/_ x A
eqrelrd2.4
|- F/_ y A
eqrelrd2.5
|- F/_ x B
eqrelrd2.6
|- F/_ y B
eqrelrd2.7
|- ( ph -> ( <. x , y >. e. A <-> <. x , y >. e. B ) )
Assertion eqrelrd2
|- ( ( ( Rel A /\ Rel B ) /\ ph ) -> A = B )

Proof

Step Hyp Ref Expression
1 eqrelrd2.1
 |-  F/ x ph
2 eqrelrd2.2
 |-  F/ y ph
3 eqrelrd2.3
 |-  F/_ x A
4 eqrelrd2.4
 |-  F/_ y A
5 eqrelrd2.5
 |-  F/_ x B
6 eqrelrd2.6
 |-  F/_ y B
7 eqrelrd2.7
 |-  ( ph -> ( <. x , y >. e. A <-> <. x , y >. e. B ) )
8 2 7 alrimi
 |-  ( ph -> A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) )
9 1 8 alrimi
 |-  ( ph -> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) )
10 9 adantl
 |-  ( ( ( Rel A /\ Rel B ) /\ ph ) -> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) )
11 1 2 3 4 5 6 ssrelf
 |-  ( Rel A -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
12 1 2 5 6 3 4 ssrelf
 |-  ( Rel B -> ( B C_ A <-> A. x A. y ( <. x , y >. e. B -> <. x , y >. e. A ) ) )
13 11 12 bi2anan9
 |-  ( ( Rel A /\ Rel B ) -> ( ( A C_ B /\ B C_ A ) <-> ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) /\ A. x A. y ( <. x , y >. e. B -> <. x , y >. e. A ) ) ) )
14 eqss
 |-  ( A = B <-> ( A C_ B /\ B C_ A ) )
15 2albiim
 |-  ( A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) <-> ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) /\ A. x A. y ( <. x , y >. e. B -> <. x , y >. e. A ) ) )
16 13 14 15 3bitr4g
 |-  ( ( Rel A /\ Rel B ) -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) )
17 16 adantr
 |-  ( ( ( Rel A /\ Rel B ) /\ ph ) -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) )
18 10 17 mpbird
 |-  ( ( ( Rel A /\ Rel B ) /\ ph ) -> A = B )