Definition df-mpt2 5432

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 3786 for two arguments. (Contributed by NM, 17-Feb-2008.)

Assertion

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

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

Allowed substitution hints:   A(x,y)   B(x,y)   𝐶(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 𝐶
6	1, 2, 3, 4, 5	cmpt2 5429	. 2 class (x ∈ A, y ∈ B ↦ 𝐶)
7	1	cv 1225	. . . . . 6 class x
8	7, 3	wcel 1369	. . . . 5 wff x ∈ A
9	2	cv 1225	. . . . . 6 class y
10	9, 4	wcel 1369	. . . . 5 wff y ∈ B
11	8, 10	wa 97	. . . 4 wff (x ∈ A ∧ y ∈ B)
12		vz	. . . . . 6 setvar z
13	12	cv 1225	. . . . 5 class z
14	13, 5	wceq 1226	. . . 4 wff z = 𝐶
15	11, 14	wa 97	. . 3 wff ((x ∈ A ∧ y ∈ B) ∧ z = 𝐶)
16	15, 1, 2, 12	coprab 5428	. 2 class {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = 𝐶)}
17	6, 16	wceq 1226	1 wff (x ∈ A, y ∈ B ↦ 𝐶) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = 𝐶)}

This definition is referenced by:  mpt2eq123  5478  mpt2eq123dva  5480  mpt2eq3dva  5483  nfmpt21  5485  nfmpt22  5486  nfmpt2  5487  mpt20  5488  cbvmpt2x  5496  mpt2v  5508  mpt2mptx  5509  resmpt2  5513  mpt2fun  5517  mpt22eqb  5524  rnmpt2  5525  reldmmpt2  5526  ovmpt4g  5537  elmpt2cl  5612  fmpt2x  5740  tposmpt2  5809  erovlem  6100  dfplpq2  6202  dfmpq2  6203