Metamath Proof Explorer


Theorem fsetabsnop

Description: The class of all functions from a (proper) singleton into B is the class 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 ( 𝑆𝑉 → { 𝑓𝑓 : { 𝑆 } ⟶ 𝐵 } = { 𝑦 ∣ ∃ 𝑏𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } } )