This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mof02

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

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

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