Theorem mofsssn

Description: There is at most one function into a subclass of a singleton. (Contributed by Zhi Wang, 24-Sep-2024)

	Ref	Expression
Assertion	mofsssn	⊢ ( 𝐵 ⊆ { 𝑌 } → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sssn	⊢ ( 𝐵 ⊆ { 𝑌 } ↔ ( 𝐵 = ∅ ∨ 𝐵 = { 𝑌 } ) )
2		mof02	⊢ ( 𝐵 = ∅ → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )
3		mofsn2	⊢ ( 𝐵 = { 𝑌 } → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )
4	2 3	jaoi	⊢ ( ( 𝐵 = ∅ ∨ 𝐵 = { 𝑌 } ) → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )
5	1 4	sylbi	⊢ ( 𝐵 ⊆ { 𝑌 } → ∃* 𝑓 𝑓 : 𝐴 ⟶ 𝐵 )