Definition df-mpo 6093

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

This definition is used by:  mpoeq123  6150  mpoeq123dva  6152  mpoeq3dva  6155  nfmpo1  6158  nfmpo2  6159  nfmpo  6160  mpo0  6161  cbvmpox  6169  mpov  6181  mpomptx  6182  resmpo  6189  mpofun  6193  mpo2eqb  6201  rnmpo  6202  reldmmpo  6203  ovmpt4g  6214  elmpocl  6287  fmpox  6440  f1od2  6475  elmpom  6478  tposmpo  6556  erovlem  6905  xpcomco  7128  dfplpq2  7727  dfmpq2  7728  mpomulf  8322