Definition df-mpo 7368

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

This definition is referenced by:  mpoeq123  7435  mpoeq123dva  7437  mpoeq3dva  7440  nfmpo1  7443  nfmpo2  7444  nfmpo  7445  0mpo0  7446  mpo0  7448  cbvmpox  7456  cbvmpov  7458  mpov  7475  mpomptx  7476  resmpo  7483  mpofun  7487  mpo2eqb  7495  rnmpo  7496  reldmmpo  7497  elrnmpores  7501  ovmpt4g  7510  mpondm0  7603  elmpocl  7604  fmpox  8016  bropopvvv  8036  bropfvvvv  8038  tposmpo  8210  erovlem  8757  xpcomco  9002  omxpenlem  9013  mpoaddf  11130  mpomulf  11131  cpnnen  16194  dmcuts  27808  mpomptxf  32777  df1stres  32803  df2ndres  32804  f1od2  32818  sxbrsigalem5  34479  cbvmpovw2  36471  cbvmpo1vw2  36472  cbvmpo2vw2  36473  cbvmpodavw2  36520  cbvmpo1davw2  36521  cbvmpo2davw2  36522  bj-dfmpoa  37477  csbmpo123  37694  uncf  37967  unccur  37971  mpobi123f  38530  cbvmpo2  45545  cbvmpo1  45546  mpomptx2  48827  cbvmpox2  48828  sectpropdlem  49527  invpropdlem  49529  isopropdlem  49531