Step |
Hyp |
Ref |
Expression |
1 |
|
id |
Could not format ( H RelPres R , S ( A , B ) -> H RelPres R , S ( A , B ) ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> H RelPres R , S ( A , B ) ) with typecode |- |
2 |
|
relpf |
Could not format ( H RelPres R , S ( A , B ) -> H : A --> B ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> H : A --> B ) with typecode |- |
3 |
|
ffun |
|
4 |
|
vex |
|
5 |
4
|
funimaex |
|
6 |
2 3 5
|
3syl |
Could not format ( H RelPres R , S ( A , B ) -> ( H " x ) e. _V ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> ( H " x ) e. _V ) with typecode |- |
7 |
1 6
|
relpfrlem |
Could not format ( H RelPres R , S ( A , B ) -> ( S Fr B -> R Fr A ) ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> ( S Fr B -> R Fr A ) ) with typecode |- |