Definition df-mpo 6090

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 4194 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 6087	. 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 6086	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1402	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is used by:  mpoeq123  6147  mpoeq123dva  6149  mpoeq3dva  6152  nfmpo1  6155  nfmpo2  6156  nfmpo  6157  mpo0  6158  cbvmpox  6166  mpov  6178  mpomptx  6179  resmpo  6186  mpofun  6190  mpo2eqb  6198  rnmpo  6199  reldmmpo  6200  ovmpt4g  6211  elmpocl  6284  fmpox  6436  f1od2  6471  elmpom  6474  tposmpo  6552  erovlem  6901  xpcomco  7124  dfplpq2  7721  dfmpq2  7722  mpomulf  8316