Step |
Hyp |
Ref |
Expression |
1 |
|
nfrelp.1 |
|
2 |
|
nfrelp.2 |
|
3 |
|
nfrelp.3 |
|
4 |
|
nfrelp.4 |
|
5 |
|
nfrelp.5 |
|
6 |
|
df-relp |
Could not format ( H RelPres R , S ( A , B ) <-> ( H : A --> B /\ A. y e. A A. z e. A ( y R z -> ( H ` y ) S ( H ` z ) ) ) ) : No typesetting found for |- ( H RelPres R , S ( A , B ) <-> ( H : A --> B /\ A. y e. A A. z e. A ( y R z -> ( H ` y ) S ( H ` z ) ) ) ) with typecode |- |
7 |
1 4 5
|
nff |
|
8 |
|
nfcv |
|
9 |
|
nfcv |
|
10 |
8 2 9
|
nfbr |
|
11 |
1 8
|
nffv |
|
12 |
1 9
|
nffv |
|
13 |
11 3 12
|
nfbr |
|
14 |
10 13
|
nfim |
|
15 |
4 14
|
nfralw |
|
16 |
4 15
|
nfralw |
|
17 |
7 16
|
nfan |
|
18 |
6 17
|
nfxfr |
Could not format F/ x H RelPres R , S ( A , B ) : No typesetting found for |- F/ x H RelPres R , S ( A , B ) with typecode |- |