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 =