This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )