Theorem bdaydm

Description: The birthday function's domain is No . (Contributed by Scott Fenton, 14-Jun-2011) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)

	Ref	Expression
Assertion	bdaydm	|- dom bday = No

Proof

Step	Hyp	Ref	Expression
1		bdayfn	|- bday Fn No
2	1	fndmi	|- dom bday = No