Description: Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | mptv | ⊢ ( 𝑥 ∈ V ↦ 𝐵 ) = { 〈 𝑥 , 𝑦 〉 ∣ 𝑦 = 𝐵 } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mpt | ⊢ ( 𝑥 ∈ V ↦ 𝐵 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ V ∧ 𝑦 = 𝐵 ) } | |
2 | vex | ⊢ 𝑥 ∈ V | |
3 | 2 | biantrur | ⊢ ( 𝑦 = 𝐵 ↔ ( 𝑥 ∈ V ∧ 𝑦 = 𝐵 ) ) |
4 | 3 | opabbii | ⊢ { 〈 𝑥 , 𝑦 〉 ∣ 𝑦 = 𝐵 } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ V ∧ 𝑦 = 𝐵 ) } |
5 | 1 4 | eqtr4i | ⊢ ( 𝑥 ∈ V ↦ 𝐵 ) = { 〈 𝑥 , 𝑦 〉 ∣ 𝑦 = 𝐵 } |