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 | ⊢ ( 𝑆 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { 〈 𝑆 , 𝑏 〉 } } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fsetsniunop | ⊢ ( 𝑆 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } = ∪ 𝑏 ∈ 𝐵 { { 〈 𝑆 , 𝑏 〉 } } ) | |
2 | iunsn | ⊢ ∪ 𝑏 ∈ 𝐵 { { 〈 𝑆 , 𝑏 〉 } } = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { 〈 𝑆 , 𝑏 〉 } } | |
3 | 1 2 | eqtrdi | ⊢ ( 𝑆 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : { 𝑆 } ⟶ 𝐵 } = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { 〈 𝑆 , 𝑏 〉 } } ) |