Theorem fsetabsnop

Description: The class of all functions from a (proper) singleton into B is the set of all the singletons of (proper) ordered pairs over the elements of B as second component. (Contributed by AV, 13-Sep-2024)

	Ref	Expression
Assertion	fsetabsnop	⊢ ( 𝑆 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } )

Proof

Step	Hyp	Ref	Expression
1		fsetsniunop	⊢ ( 𝑆 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } = ∪ 𝑏 ∈ 𝐵 { { ⟨ 𝑆 , 𝑏 ⟩ } } )
2		iunsn	⊢ ∪ 𝑏 ∈ 𝐵 { { ⟨ 𝑆 , 𝑏 ⟩ } } = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } }
3	1 2	eqtrdi	⊢ ( 𝑆 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } )