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

Metamath Proof Explorer

Theorem mof0ALT

Description: Alternate proof of mof0 with stronger requirements on distinct variables. Uses mo4 . (Contributed by Zhi Wang, 19-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	mof0ALT	$⊢ \exists^{*} f f : A ⟶ \emptyset$

Proof

Step	Hyp	Ref	Expression
1		f00	$⊢ f : A ⟶ \emptyset \leftrightarrow (f = \emptyset \land A = \emptyset)$
2	1	simplbi	$⊢ f : A ⟶ \emptyset \to f = \emptyset$
3		f00	$⊢ g : A ⟶ \emptyset \leftrightarrow (g = \emptyset \land A = \emptyset)$
4	3	simplbi	$⊢ g : A ⟶ \emptyset \to g = \emptyset$
5		eqtr3	$⊢ (f = \emptyset \land g = \emptyset) \to f = g$
6	2 4 5	syl2an	$⊢ (f : A ⟶ \emptyset \land g : A ⟶ \emptyset) \to f = g$
7	6	gen2	$⊢ \forall f \forall g ((f : A ⟶ \emptyset \land g : A ⟶ \emptyset) \to f = g)$
8		feq1	$⊢ f = g \to (f : A ⟶ \emptyset \leftrightarrow g : A ⟶ \emptyset)$
9	8	mo4	$⊢ \exists^{*} f f : A ⟶ \emptyset \leftrightarrow \forall f \forall g ((f : A ⟶ \emptyset \land g : A ⟶ \emptyset) \to f = g)$
10	7 9	mpbir	$⊢ \exists^{*} f f : A ⟶ \emptyset$