Definition df-mpo 7358

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

This definition is referenced by:  mpoeq123  7425  mpoeq123dva  7427  mpoeq3dva  7430  nfmpo1  7433  nfmpo2  7434  nfmpo  7435  0mpo0  7436  mpo0  7438  cbvmpox  7446  cbvmpov  7448  mpov  7465  mpomptx  7466  resmpo  7473  mpofun  7477  mpo2eqb  7485  rnmpo  7486  reldmmpo  7487  elrnmpores  7491  ovmpt4g  7500  mpondm0  7593  elmpocl  7594  fmpox  8009  bropopvvv  8030  bropfvvvv  8032  tposmpo  8203  erovlem  8747  xpcomco  8991  omxpenlem  9002  mpoaddf  11122  mpomulf  11123  cpnnen  16156  dmscut  27740  mpomptxf  32634  df1stres  32660  df2ndres  32661  f1od2  32677  sxbrsigalem5  34255  cbvmpovw2  36215  cbvmpo1vw2  36216  cbvmpo2vw2  36217  cbvmpodavw2  36264  cbvmpo1davw2  36265  cbvmpo2davw2  36266  bj-dfmpoa  37091  csbmpo123  37304  uncf  37578  unccur  37582  mpobi123f  38141  cbvmpo2  45075  cbvmpo1  45076  mpomptx2  48307  cbvmpox2  48308  sectpropdlem  49009  invpropdlem  49011  isopropdlem  49013