Metamath Proof Explorer


Theorem mpov

Description: Operation with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013)

Ref Expression
Assertion mpov ( 𝑥 ∈ V , 𝑦 ∈ V ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝐶 }

Proof

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 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝐶 }