Step |
Hyp |
Ref |
Expression |
1 |
|
breq |
|- ( R = S -> ( z R y <-> z S y ) ) |
2 |
1
|
notbid |
|- ( R = S -> ( -. z R y <-> -. z S y ) ) |
3 |
2
|
rexralbidv |
|- ( R = S -> ( E. y e. x A. z e. x -. z R y <-> E. y e. x A. z e. x -. z S y ) ) |
4 |
3
|
imbi2d |
|- ( R = S -> ( ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) <-> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z S y ) ) ) |
5 |
4
|
albidv |
|- ( R = S -> ( A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z S y ) ) ) |
6 |
|
df-fr |
|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) ) |
7 |
|
df-fr |
|- ( S Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z S y ) ) |
8 |
5 6 7
|
3bitr4g |
|- ( R = S -> ( R Fr A <-> S Fr A ) ) |