Definition df-mpt2 5437

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 3790 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 5434	. 2 class (x ∈ A, y ∈ B ↦ 𝐶)
7	1	cv 1225	. . . . . 6 class x
8	7, 3	wcel 1370	. . . . 5 wff x ∈ A
9	2	cv 1225	. . . . . 6 class y
10	9, 4	wcel 1370	. . . . 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 5433	. 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  5483  mpt2eq123dva  5485  mpt2eq3dva  5488  nfmpt21  5490  nfmpt22  5491  nfmpt2  5492  mpt20  5493  cbvmpt2x  5501  mpt2v  5513  mpt2mptx  5514  resmpt2  5518  mpt2fun  5522  mpt22eqb  5529  rnmpt2  5530  reldmmpt2  5531  ovmpt4g  5542  elmpt2cl  5617  fmpt2x  5745  tposmpt2  5814  erovlem  6105  dfplpq2  6207  dfmpq2  6208