Description: The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | fvtp2g | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tprot | |
|
2 | 1 | fveq1i | |
3 | necom | |
|
4 | fvtp1g | |
|
5 | 4 | expcom | |
6 | 5 | ancoms | |
7 | 3 6 | sylanb | |
8 | 7 | impcom | |
9 | 2 8 | eqtrid | |