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