Description: The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | fvpr0o | |- ( A e. V -> ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) = A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | peano1 | |- (/) e. _om |
|
2 | 1n0 | |- 1o =/= (/) |
|
3 | 2 | necomi | |- (/) =/= 1o |
4 | fvpr1g | |- ( ( (/) e. _om /\ A e. V /\ (/) =/= 1o ) -> ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) = A ) |
|
5 | 1 3 4 | mp3an13 | |- ( A e. V -> ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) = A ) |