Step |
Hyp |
Ref |
Expression |
1 |
|
feq3 |
|
2 |
1
|
anbi1d |
|
3 |
|
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 |- |
4 |
|
df-relp |
Could not format ( H RelPres R , S ( A , C ) <-> ( H : A --> C /\ 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 , C ) <-> ( H : A --> C /\ A. x e. A A. y e. A ( x R y -> ( H ` x ) S ( H ` y ) ) ) ) with typecode |- |
5 |
2 3 4
|
3bitr4g |
Could not format ( B = C -> ( H RelPres R , S ( A , B ) <-> H RelPres R , S ( A , C ) ) ) : No typesetting found for |- ( B = C -> ( H RelPres R , S ( A , B ) <-> H RelPres R , S ( A , C ) ) ) with typecode |- |