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 | |- ( (/) ^m (/) ) = { (/) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f0bi | |- ( f : (/) --> (/) <-> f = (/) ) |
|
2 | 1 | abbii | |- { f | f : (/) --> (/) } = { f | f = (/) } |
3 | 0ex | |- (/) e. _V |
|
4 | 3 3 | mapval | |- ( (/) ^m (/) ) = { f | f : (/) --> (/) } |
5 | df-sn | |- { (/) } = { f | f = (/) } |
|
6 | 2 4 5 | 3eqtr4i | |- ( (/) ^m (/) ) = { (/) } |