Metamath Proof Explorer

Theorem mpov

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

Ref Expression
Assertion mpov ⊢ x ∈ V , y ∈ V ⟼ C = x y z | z = C

Proof

Step Hyp Ref Expression
1 df-mpo ⊢ x ∈ V , y ∈ V ⟼ C = x y z | x ∈ V ∧ y ∈ V ∧ z = C
2 vex ⊢ x ∈ V
3 vex ⊢ y ∈ V
4 2 3 pm3.2i ⊢ x ∈ V ∧ y ∈ V
5 4 biantrur ⊢ z = C ↔ x ∈ V ∧ y ∈ V ∧ z = C
6 5 oprabbii ⊢ x y z | z = C = x y z | x ∈ V ∧ y ∈ V ∧ z = C
7 1 6 eqtr4i ⊢ x ∈ V , y ∈ V ⟼ C = x y z | z = C