Metamath Proof Explorer


Theorem bdayfun

Description: The birthday function is a function. (Contributed by Scott Fenton, 14-Jun-2011)

Ref Expression
Assertion bdayfun Fun bday

Proof

Step Hyp Ref Expression
1 bdayfo bday : No onto→ On
2 fofun ( bday : No onto→ On → Fun bday )
3 1 2 ax-mp Fun bday