Definition df-mpt2 5460

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 3811 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 5457	. 2 class (x ∈ A, y ∈ B ↦ 𝐶)
7	1	cv 1241	. . . . . 6 class x
8	7, 3	wcel 1390	. . . . 5 wff x ∈ A
9	2	cv 1241	. . . . . 6 class y
10	9, 4	wcel 1390	. . . . 5 wff y ∈ B
11	8, 10	wa 97	. . . 4 wff (x ∈ A ∧ y ∈ B)
12		vz	. . . . . 6 setvar z
13	12	cv 1241	. . . . 5 class z
14	13, 5	wceq 1242	. . . 4 wff z = 𝐶
15	11, 14	wa 97	. . 3 wff ((x ∈ A ∧ y ∈ B) ∧ z = 𝐶)
16	15, 1, 2, 12	coprab 5456	. 2 class {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = 𝐶)}
17	6, 16	wceq 1242	1 wff (x ∈ A, y ∈ B ↦ 𝐶) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = 𝐶)}

This definition is referenced by:  mpt2eq123  5506  mpt2eq123dva  5508  mpt2eq3dva  5511  nfmpt21  5513  nfmpt22  5514  nfmpt2  5515  mpt20  5516  cbvmpt2x  5524  mpt2v  5536  mpt2mptx  5537  resmpt2  5541  mpt2fun  5545  mpt22eqb  5552  rnmpt2  5553  reldmmpt2  5554  ovmpt4g  5565  elmpt2cl  5640  fmpt2x  5768  tposmpt2  5837  erovlem  6134  xpcomco  6236  dfplpq2  6338  dfmpq2  6339