Theorem mof02

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

	Ref	Expression
Assertion	mof02	|- ( B = (/) -> E* f f : A --> B )

Proof

Step	Hyp	Ref	Expression
1		mof0	|- E* f f : A --> (/)
2		feq3	|- ( B = (/) -> ( f : A --> B <-> f : A --> (/) ) )
3	2	mobidv	|- ( B = (/) -> ( E* f f : A --> B <-> E* f f : A --> (/) ) )
4	1 3	mpbiri	|- ( B = (/) -> E* f f : A --> B )