Step |
Hyp |
Ref |
Expression |
0 |
|
cH |
|
1 |
|
cR |
|
2 |
|
cS |
|
3 |
|
cA |
|
4 |
|
cB |
|
5 |
3 4 1 2 0
|
wrelp |
Could not format H RelPres R , S ( A , B ) : No typesetting found for wff H RelPres R , S ( A , B ) with typecode wff |
6 |
3 4 0
|
wf |
|
7 |
|
vx |
|
8 |
|
vy |
|
9 |
7
|
cv |
|
10 |
8
|
cv |
|
11 |
9 10 1
|
wbr |
|
12 |
9 0
|
cfv |
|
13 |
10 0
|
cfv |
|
14 |
12 13 2
|
wbr |
|
15 |
11 14
|
wi |
|
16 |
15 8 3
|
wral |
|
17 |
16 7 3
|
wral |
|
18 |
6 17
|
wa |
|
19 |
5 18
|
wb |
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 wff ( 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 wff |