Definition df-mpo 5731

Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from 𝑥, 𝑦 (in 𝐴 × 𝐵) to 𝐵(𝑥, 𝑦)." An extension of df-mpt 3949 for two arguments. (Contributed by NM, 17-Feb-2008.)

Assertion

Ref	Expression
df-mpo	⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

Distinct variable groups:   𝑥,𝑧   𝑦,𝑧   𝑧,𝐴   𝑧,𝐵   𝑧,𝐶

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)

Detailed syntax breakdown of Definition df-mpo

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		vy	. . 3 setvar 𝑦
3		cA	. . 3 class 𝐴
4		cB	. . 3 class 𝐵
5		cC	. . 3 class 𝐶
6	1, 2, 3, 4, 5	cmpo 5728	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1311	. . . . . 6 class 𝑥
8	7, 3	wcel 1461	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1311	. . . . . 6 class 𝑦
10	9, 4	wcel 1461	. . . . 5 wff 𝑦 ∈ 𝐵
11	8, 10	wa 103	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
12		vz	. . . . . 6 setvar 𝑧
13	12	cv 1311	. . . . 5 class 𝑧
14	13, 5	wceq 1312	. . . 4 wff 𝑧 = 𝐶
15	11, 14	wa 103	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
16	15, 1, 2, 12	coprab 5727	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1312	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is referenced by:  mpoeq123  5782  mpoeq123dva  5784  mpoeq3dva  5787  nfmpo1  5790  nfmpo2  5791  nfmpo  5792  mpo0  5793  cbvmpox  5801  mpov  5813  mpomptx  5814  resmpo  5821  mpofun  5825  mpo2eqb  5832  rnmpo  5833  reldmmpo  5834  ovmpt4g  5845  elmpocl  5920  fmpox  6050  f1od2  6084  tposmpo  6130  erovlem  6473  xpcomco  6671  dfplpq2  7104  dfmpq2  7105