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