Definition df-mpo 7428

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 5198 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 7425	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1569	. . . . . 6 class 𝑥
8	7, 3	wcel 2146	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1569	. . . . . 6 class 𝑦
10	9, 4	wcel 2146	. . . . 5 wff 𝑦 ∈ 𝐵
11	8, 10	wa 401	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
12		vz	. . . . . 6 setvar 𝑧
13	12	cv 1569	. . . . 5 class 𝑧
14	13, 5	wceq 1570	. . . 4 wff 𝑧 = 𝐶
15	11, 14	wa 401	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
16	15, 1, 2, 12	coprab 7424	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1570	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is used by:  mpoeq123  7495  mpoeq123dva  7497  mpoeq3dva  7500  nfmpo1  7503  nfmpo2  7504  nfmpo  7505  0mpo0  7506  mpo0  7508  cbvmpox  7516  cbvmpov  7518  mpov  7535  mpomptx  7536  resmpo  7543  mpofun  7547  mpo2eqb  7555  rnmpo  7556  reldmmpo  7557  elrnmpores  7561  ovmpt4g  7570  mpondm0  7663  elmpocl  7664  fmpox  8073  bropopvvv  8094  bropfvvvv  8096  tposmpo  8268  erovlem  8820  xpcomco  9065  omxpenlem  9076  mpoaddf  11212  mpomulf  11213  cpnnen  16310  dmcuts  28014  mpomptxf  33053  df1stres  33079  df2ndres  33080  f1od2  33094  sxbrsigalem5  34702  cbvmpovw2  36787  cbvmpo1vw2  36788  cbvmpo2vw2  36789  cbvmpodavw2  36836  cbvmpo1davw2  36837  cbvmpo2davw2  36838  bj-dfmpoa  37793  csbmpo123  38010  uncf  38283  unccur  38287  mpobi123f  38844  cbvmpo2  45848  cbvmpo1  45849  mpomptx2  49148  cbvmpox2  49149  sectpropdlem  49847  invpropdlem  49849  isopropdlem  49851