Metamath Proof Explorer

Theorem fset0

Description: The set of functions from the empty set is the singleton containing the empty set. (Contributed by AV, 13-Sep-2024)

Ref Expression
Assertion fset0 
|- { f | f : (/) --> B } = { (/) }

Proof

Step Hyp Ref Expression
1 f0bi 
 |-  ( f : (/) --> B <-> f = (/) )
2 1 abbii 
 |-  { f | f : (/) --> B } = { f | f = (/) }
3 df-sn 
 |-  { (/) } = { f | f = (/) }
4 2 3 eqtr4i 
 |-  { f | f : (/) --> B } = { (/) }