Definition df-mpo 5901

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 4081 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 5898	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1363	. . . . . 6 class 𝑥
8	7, 3	wcel 2160	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1363	. . . . . 6 class 𝑦
10	9, 4	wcel 2160	. . . . 5 wff 𝑦 ∈ 𝐵
11	8, 10	wa 104	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
12		vz	. . . . . 6 setvar 𝑧
13	12	cv 1363	. . . . 5 class 𝑧
14	13, 5	wceq 1364	. . . 4 wff 𝑧 = 𝐶
15	11, 14	wa 104	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
16	15, 1, 2, 12	coprab 5897	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1364	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is referenced by:  mpoeq123  5955  mpoeq123dva  5957  mpoeq3dva  5960  nfmpo1  5963  nfmpo2  5964  nfmpo  5965  mpo0  5966  cbvmpox  5974  mpov  5986  mpomptx  5987  resmpo  5994  mpofun  5998  mpo2eqb  6006  rnmpo  6007  reldmmpo  6008  ovmpt4g  6019  elmpocl  6091  fmpox  6225  f1od2  6260  tposmpo  6306  erovlem  6653  xpcomco  6852  dfplpq2  7383  dfmpq2  7384