Definition df-mpo 7161

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 5117 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 7158	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1537	. . . . . 6 class 𝑥
8	7, 3	wcel 2111	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1537	. . . . . 6 class 𝑦
10	9, 4	wcel 2111	. . . . 5 wff 𝑦 ∈ 𝐵
11	8, 10	wa 399	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
12		vz	. . . . . 6 setvar 𝑧
13	12	cv 1537	. . . . 5 class 𝑧
14	13, 5	wceq 1538	. . . 4 wff 𝑧 = 𝐶
15	11, 14	wa 399	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
16	15, 1, 2, 12	coprab 7157	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1538	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is referenced by:  mpoeq123  7226  mpoeq123dva  7228  mpoeq3dva  7231  nfmpo1  7234  nfmpo2  7235  nfmpo  7236  0mpo0  7237  mpo0  7239  cbvmpox  7247  mpov  7264  mpomptx  7265  resmpo  7272  mpofun  7276  mpofunOLD  7277  mpo2eqb  7284  rnmpo  7285  reldmmpo  7286  elrnmpores  7289  ovmpt4g  7298  mpondm0  7388  elmpocl  7389  fmpox  7775  bropopvvv  7796  bropfvvvv  7798  tposmpo  7945  erovlem  8409  xpcomco  8641  omxpenlem  8652  cpnnen  15643  mpomptxf  30552  df1stres  30572  df2ndres  30573  f1od2  30592  sxbrsigalem5  31786  dmscut  33600  bj-dfmpoa  34847  csbmpo123  35062  uncf  35350  unccur  35354  mpobi123f  35914  cbvmpo2  42141  cbvmpo1  42142  mpomptx2  45152  cbvmpox2  45153