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 =

Proof

Step Hyp Ref Expression
1 f0bi f : f =
2 1 abbii f | f : = f | f =
3 0ex V
4 3 3 mapval = f | f :
5 df-sn = f | f =
6 2 4 5 3eqtr4i =