Definition df-mpo 7413

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 5186 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 7410	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1569	. . . . . 6 class 𝑥
8	7, 3	wcel 2145	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1569	. . . . . 6 class 𝑦
10	9, 4	wcel 2145	. . . . 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 7409	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1570	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is used by:  mpoeq123  7480  mpoeq123dva  7482  mpoeq3dva  7485  nfmpo1  7488  nfmpo2  7489  nfmpo  7490  0mpo0  7491  mpo0  7493  cbvmpox  7501  cbvmpov  7503  mpov  7520  mpomptx  7521  resmpo  7528  mpofun  7532  mpo2eqb  7540  rnmpo  7541  reldmmpo  7542  elrnmpores  7546  ovmpt4g  7555  mpondm0  7649  elmpocl  7650  fmpox  8061  bropopvvv  8084  bropfvvvv  8086  tposmpo  8258  erovlem  8812  uncf  8869  xpcomco  9064  omxpenlem  9075  mpoaddf  11266  mpomulf  11267  cpnnen  16365  dmcuts  28111  mpomptxf  33206  df1stres  33231  df2ndres  33232  f1od2  33245  sxbrsigalem5  34855  cbvmpovw2  36953  cbvmpo1vw2  36954  cbvmpo2vw2  36955  cbvmpodavw2  37002  cbvmpo1davw2  37003  cbvmpo2davw2  37004  bj-dfmpoa  37959  csbmpo123  38174  unccur  38446  mpobi123f  39014  cbvmpo2  46033  cbvmpo1  46034  mpomptx2  49369  cbvmpox2  49370  sectpropdlem  50066  invpropdlem  50068  isopropdlem  50070