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 )