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

Metamath Proof Explorer

Theorem f0bi

Description: A function with empty domain is empty. (Contributed by Alexander van der Vekens, 30-Jun-2018)

		Ref	Expression
	Assertion	f0bi	$⊢ F : \emptyset ⟶ X \leftrightarrow F = \emptyset$

Step	Hyp	Ref	Expression
1		ffn	$⊢ F : \emptyset ⟶ X \to F Fn \emptyset$
2		fn0	$⊢ F Fn \emptyset \leftrightarrow F = \emptyset$
3	1 2	sylib	$⊢ F : \emptyset ⟶ X \to F = \emptyset$
4		f0	$⊢ \emptyset : \emptyset ⟶ X$
5		feq1	$⊢ F = \emptyset \to (F : \emptyset ⟶ X \leftrightarrow \emptyset : \emptyset ⟶ X)$
6	4 5	mpbiri	$⊢ F = \emptyset \to F : \emptyset ⟶ X$
7	3 6	impbii	$⊢ F : \emptyset ⟶ X \leftrightarrow F = \emptyset$