Definition df-mpo 7280

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

This definition is referenced by:  mpoeq123  7347  mpoeq123dva  7349  mpoeq3dva  7352  nfmpo1  7355  nfmpo2  7356  nfmpo  7357  0mpo0  7358  mpo0  7360  cbvmpox  7368  mpov  7386  mpomptx  7387  resmpo  7394  mpofun  7398  mpofunOLD  7399  mpo2eqb  7406  rnmpo  7407  reldmmpo  7408  elrnmpores  7411  ovmpt4g  7420  mpondm0  7510  elmpocl  7511  fmpox  7907  bropopvvv  7930  bropfvvvv  7932  tposmpo  8079  erovlem  8602  xpcomco  8849  omxpenlem  8860  cpnnen  15938  mpomptxf  31016  df1stres  31036  df2ndres  31037  f1od2  31056  sxbrsigalem5  32255  dmscut  34005  bj-dfmpoa  35289  csbmpo123  35502  uncf  35756  unccur  35760  mpobi123f  36320  cbvmpo2  42647  cbvmpo1  42648  mpomptx2  45670  cbvmpox2  45671