Theorem mof0

Description: There is at most one function into the empty set. (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Assertion	mof0	$$⊢{\exists }^{*}ff:A⟶\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		eqeq2	$$⊢g=\varnothing \to \left(f=g\leftrightarrow f=\varnothing \right)$$
3	2	imbi2d	$$⊢g=\varnothing \to \left(\left(f:A⟶\varnothing \to f=g\right)\leftrightarrow \left(f:A⟶\varnothing \to f=\varnothing \right)\right)$$
4	3	albidv	$$⊢g=\varnothing \to \left(\forall f\left(f:A⟶\varnothing \to f=g\right)\leftrightarrow \forall f\left(f:A⟶\varnothing \to f=\varnothing \right)\right)$$
5	1 4	spcev	$$⊢\forall f\left(f:A⟶\varnothing \to f=\varnothing \right)\to \exists g\forall f\left(f:A⟶\varnothing \to f=g\right)$$
6		f00	$$⊢f:A⟶\varnothing \leftrightarrow \left(f=\varnothing \wedge A=\varnothing \right)$$
7	6	simplbi	$$⊢f:A⟶\varnothing \to f=\varnothing$$
8	5 7	mpg	$$⊢\exists g\forall f\left(f:A⟶\varnothing \to f=g\right)$$
9		df-mo	$$⊢{\exists }^{*}ff:A⟶\varnothing \leftrightarrow \exists g\forall f\left(f:A⟶\varnothing \to f=g\right)$$
10	8 9	mpbir	$$⊢{\exists }^{*}ff:A⟶\varnothing$$