Description: Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | mpov | ⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ 𝐶 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝑧 = 𝐶 } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mpo | ⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ 𝐶 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ∧ 𝑧 = 𝐶 ) } | |
2 | vex | ⊢ 𝑥 ∈ V | |
3 | vex | ⊢ 𝑦 ∈ V | |
4 | 2 3 | pm3.2i | ⊢ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) |
5 | 4 | biantrur | ⊢ ( 𝑧 = 𝐶 ↔ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ∧ 𝑧 = 𝐶 ) ) |
6 | 5 | oprabbii | ⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝑧 = 𝐶 } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ∧ 𝑧 = 𝐶 ) } |
7 | 1 6 | eqtr4i | ⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ 𝐶 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝑧 = 𝐶 } |