This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-mpo

Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x , y (in A X. B ) to C ( x , y ) ". An extension of df-mpt for two arguments. (Contributed by NM, 17-Feb-2008)

Ref Expression
Assertion df-mpo ⊢ x ∈ A , y ∈ B ⟼ C = x y z | x ∈ A ∧ y ∈ B ∧ z = C

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvar x
1 cA class A
2 vy setvar y
3 cB class B
4 cC class C
5 0 2 1 3 4 cmpo class x ∈ A , y ∈ B ⟼ C
6 vz setvar z
7 0 cv setvar x
8 7 1 wcel wff x ∈ A
9 2 cv setvar y
10 9 3 wcel wff y ∈ B
11 8 10 wa wff x ∈ A ∧ y ∈ B
12 6 cv setvar z
13 12 4 wceq wff z = C
14 11 13 wa wff x ∈ A ∧ y ∈ B ∧ z = C
15 14 0 2 6 coprab class x y z | x ∈ A ∧ y ∈ B ∧ z = C
16 5 15 wceq wff x ∈ A , y ∈ B ⟼ C = x y z | x ∈ A ∧ y ∈ B ∧ z = C