Theorem mof02

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

	Ref	Expression
Assertion	mof02	⊢ ( 𝐵 = ∅ → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mof0	⊢ ∃* 𝑓 𝑓 : 𝐴 ⟶ ∅
2		feq3	⊢ ( 𝐵 = ∅ → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ 𝑓 : 𝐴 ⟶ ∅ ) )
3	2	mobidv	⊢ ( 𝐵 = ∅ → ( ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 ↔ ∃* 𝑓 𝑓 : 𝐴 ⟶ ∅ ) )
4	1 3	mpbiri	⊢ ( 𝐵 = ∅ → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )