Metamath Proof Explorer
Description: The set of mappings of the empty set to the empty set is the singleton
containing the empty set. (Contributed by AV, 31-Mar-2024)
|
|
Ref |
Expression |
|
Assertion |
0map0sn0 |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
f0bi |
|
2 |
1
|
abbii |
|
3 |
|
0ex |
|
4 |
3 3
|
mapval |
|
5 |
|
df-sn |
|
6 |
2 4 5
|
3eqtr4i |
|