Metamath Proof Explorer


Theorem 0map0sn0

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 (/) ) = { (/) }

Proof

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 (/) ) = { (/) }