Definition df-mpo 7414

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 5233 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 7411	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1541	. . . . . 6 class 𝑥
8	7, 3	wcel 2107	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1541	. . . . . 6 class 𝑦
10	9, 4	wcel 2107	. . . . 5 wff 𝑦 ∈ 𝐵
11	8, 10	wa 397	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
12		vz	. . . . . 6 setvar 𝑧
13	12	cv 1541	. . . . 5 class 𝑧
14	13, 5	wceq 1542	. . . 4 wff 𝑧 = 𝐶
15	11, 14	wa 397	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
16	15, 1, 2, 12	coprab 7410	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1542	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is referenced by:  mpoeq123  7481  mpoeq123dva  7483  mpoeq3dva  7486  nfmpo1  7489  nfmpo2  7490  nfmpo  7491  0mpo0  7492  mpo0  7494  cbvmpox  7502  mpov  7520  mpomptx  7521  resmpo  7528  mpofun  7532  mpofunOLD  7533  mpo2eqb  7541  rnmpo  7542  reldmmpo  7543  elrnmpores  7546  ovmpt4g  7555  mpondm0  7647  elmpocl  7648  fmpox  8053  bropopvvv  8076  bropfvvvv  8078  tposmpo  8248  erovlem  8807  xpcomco  9062  omxpenlem  9073  cpnnen  16172  dmscut  27313  mpomptxf  31936  df1stres  31956  df2ndres  31957  f1od2  31977  sxbrsigalem5  33318  mpomulf  35190  mpoaddf  35216  bj-dfmpoa  36047  csbmpo123  36260  uncf  36515  unccur  36519  mpobi123f  37078  cbvmpo2  43834  cbvmpo1  43835  mpomptx2  47058  cbvmpox2  47059