Metamath Proof Explorer
Description: Function value (Theorem 6.12(1) of TakeutiZaring p. 27), analogous to
tz6.12-1 . (Contributed by AV, 5-Sep-2022)
|
|
Ref |
Expression |
|
Assertion |
tz6.12-1-afv2 |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
df-br |
|
2 |
1
|
eubii |
|
3 |
|
tz6.12-afv2 |
|
4 |
1 2 3
|
syl2anb |
|