Definition df-mpt2 5655

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 × B) to B(x, y)." An extension of df-mpt 5653 for two arguments. (Contributed by SF, 5-Jan-2015.)

Assertion

Ref	Expression
df-mpt2	⊢ (x ∈ A, y ∈ B ↦ C) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = C)}

Distinct variable groups:   x,z   y,z   z,A   z,B   z,C

Allowed substitution hints:   A(x,y)   B(x,y)   C(x,y)

Detailed syntax breakdown of Definition df-mpt2

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar x
2		vy	. . 3 setvar y
3		cA	. . 3 class A
4		cB	. . 3 class B
5		cC	. . 3 class C
6	1, 2, 3, 4, 5	cmpt2 5654	. 2 class (x ∈ A, y ∈ B ↦ C)
7	1	cv 1641	. . . . . 6 class x
8	7, 3	wcel 1710	. . . . 5 wff x ∈ A
9	2	cv 1641	. . . . . 6 class y
10	9, 4	wcel 1710	. . . . 5 wff y ∈ B
11	8, 10	wa 358	. . . 4 wff (x ∈ A ∧ y ∈ B)
12		vz	. . . . . 6 setvar z
13	12	cv 1641	. . . . 5 class z
14	13, 5	wceq 1642	. . . 4 wff z = C
15	11, 14	wa 358	. . 3 wff ((x ∈ A ∧ y ∈ B) ∧ z = C)
16	15, 1, 2, 12	coprab 5528	. 2 class {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = C)}
17	6, 16	wceq 1642	1 wff (x ∈ A, y ∈ B ↦ C) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = C)}

This definition is referenced by:  mpt2eq123  5662  mpt2eq123dv  5664  mpt2eq3dva  5670  nfmpt21  5674  nfmpt22  5675  nfmpt2  5676  cbvmpt2x  5679  resmpt2  5698  fnov2  5708  mpt2mptx  5709  ovmpt4g  5711  ovmpt2x  5713  ovmpt2ga  5714  rnmpt2  5718  mpt2v  5720  fmpt2x  5731  releqmpt2  5810  composefn  5819  fnce  6177