Step |
Hyp |
Ref |
Expression |
1 |
|
eqbrrdv.1 |
|- ( ph -> Rel A ) |
2 |
|
eqbrrdv.2 |
|- ( ph -> Rel B ) |
3 |
|
eqbrrdv.3 |
|- ( ph -> ( x A y <-> x B y ) ) |
4 |
|
df-br |
|- ( x A y <-> <. x , y >. e. A ) |
5 |
|
df-br |
|- ( x B y <-> <. x , y >. e. B ) |
6 |
3 4 5
|
3bitr3g |
|- ( ph -> ( <. x , y >. e. A <-> <. x , y >. e. B ) ) |
7 |
6
|
alrimivv |
|- ( ph -> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) |
8 |
|
eqrel |
|- ( ( Rel A /\ Rel B ) -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) ) |
9 |
1 2 8
|
syl2anc |
|- ( ph -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) ) |
10 |
7 9
|
mpbird |
|- ( ph -> A = B ) |