Metamath Proof Explorer

Theorem eqrelf

Description: The equality connective between relations. (Contributed by Peter Mazsa, 25-Jun-2019)

Ref Expression
Hypotheses eqrelf.1 
|- F/_ x A
eqrelf.2 
|- F/_ x B
eqrelf.3 
|- F/_ y A
eqrelf.4 
|- F/_ y B
Assertion eqrelf 
|- ( ( Rel A /\ Rel B ) -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) )

Proof

Step Hyp Ref Expression
1 eqrelf.1 
 |-  F/_ x A
2 eqrelf.2 
 |-  F/_ x B
3 eqrelf.3 
 |-  F/_ y A
4 eqrelf.4 
 |-  F/_ y B
5 eqrel 
 |-  ( ( Rel A /\ Rel B ) -> ( A = B <-> A. u A. v ( <. u , v >. e. A <-> <. u , v >. e. B ) ) )
6 nfv 
 |-  F/ u ( <. x , y >. e. A <-> <. x , y >. e. B )
7 nfv 
 |-  F/ v ( <. x , y >. e. A <-> <. x , y >. e. B )
8 1 nfel2 
 |-  F/ x <. u , v >. e. A
9 2 nfel2 
 |-  F/ x <. u , v >. e. B
10 8 9 nfbi 
 |-  F/ x ( <. u , v >. e. A <-> <. u , v >. e. B )
11 3 nfel2 
 |-  F/ y <. u , v >. e. A
12 4 nfel2 
 |-  F/ y <. u , v >. e. B
13 11 12 nfbi 
 |-  F/ y ( <. u , v >. e. A <-> <. u , v >. e. B )
14 opeq12 
 |-  ( ( x = u /\ y = v ) -> <. x , y >. = <. u , v >. )
15 14 eleq1d 
 |-  ( ( x = u /\ y = v ) -> ( <. x , y >. e. A <-> <. u , v >. e. A ) )
16 14 eleq1d 
 |-  ( ( x = u /\ y = v ) -> ( <. x , y >. e. B <-> <. u , v >. e. B ) )
17 15 16 bibi12d 
 |-  ( ( x = u /\ y = v ) -> ( ( <. x , y >. e. A <-> <. x , y >. e. B ) <-> ( <. u , v >. e. A <-> <. u , v >. e. B ) ) )
18 6 7 10 13 17 cbval2v 
 |-  ( A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) <-> A. u A. v ( <. u , v >. e. A <-> <. u , v >. e. B ) )
19 5 18 bitr4di 
 |-  ( ( Rel A /\ Rel B ) -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) )