Step |
Hyp |
Ref |
Expression |
1 |
|
feq1 |
|
2 |
|
fveq1 |
|
3 |
|
fveq1 |
|
4 |
2 3
|
breq12d |
|
5 |
4
|
imbi2d |
|
6 |
5
|
2ralbidv |
|
7 |
1 6
|
anbi12d |
|
8 |
|
df-relp |
Could not format ( H RelPres R , S ( A , B ) <-> ( H : A --> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) : No typesetting found for |- ( H RelPres R , S ( A , B ) <-> ( H : A --> B /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) with typecode |- |
9 |
|
df-relp |
Could not format ( G RelPres R , S ( A , B ) <-> ( G : A --> B /\ A. x e. A A. y e. A ( x R y -> ( G ` x ) S ( G ` y ) ) ) ) : No typesetting found for |- ( G RelPres R , S ( A , B ) <-> ( G : A --> B /\ A. x e. A A. y e. A ( x R y -> ( G ` x ) S ( G ` y ) ) ) ) with typecode |- |
10 |
7 8 9
|
3bitr4g |
Could not format ( H = G -> ( H RelPres R , S ( A , B ) <-> G RelPres R , S ( A , B ) ) ) : No typesetting found for |- ( H = G -> ( H RelPres R , S ( A , B ) <-> G RelPres R , S ( A , B ) ) ) with typecode |- |