Theorem mof02

Description: A variant of mof0 . (Contributed by Zhi Wang, 20-Sep-2024)

	Ref	Expression
Assertion	mof02	$$⊢B=\varnothing \to {\exists }^{*}ff:A⟶B$$

Proof

Step	Hyp	Ref	Expression
1		mof0	$$⊢{\exists }^{*}ff:A⟶\varnothing$$
2		feq3	$$⊢B=\varnothing \to \left(f:A⟶B\leftrightarrow f:A⟶\varnothing \right)$$
3	2	mobidv	$$⊢B=\varnothing \to \left({\exists }^{*}ff:A⟶B\leftrightarrow {\exists }^{*}ff:A⟶\varnothing \right)$$
4	1 3	mpbiri	$$⊢B=\varnothing \to {\exists }^{*}ff:A⟶B$$