Theorem mof0ALT

Description: Alternate proof for 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 }^{*}ff:A⟶\varnothing$$

Proof

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