Definition df-mpt2 5537

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 3841 for two arguments. (Contributed by NM, 17-Feb-2008.)

Assertion

Ref	Expression
df-mpt2	⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

Distinct variable groups:   𝑥,𝑧   𝑦,𝑧   𝑧,𝐴   𝑧,𝐵   𝑧,𝐶

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)

Detailed syntax breakdown of Definition df-mpt2

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	cmpt2 5534	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1283	. . . . . 6 class 𝑥
8	7, 3	wcel 1433	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1283	. . . . . 6 class 𝑦
10	9, 4	wcel 1433	. . . . 5 wff 𝑦 ∈ 𝐵
11	8, 10	wa 102	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
12		vz	. . . . . 6 setvar 𝑧
13	12	cv 1283	. . . . 5 class 𝑧
14	13, 5	wceq 1284	. . . 4 wff 𝑧 = 𝐶
15	11, 14	wa 102	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
16	15, 1, 2, 12	coprab 5533	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1284	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is referenced by:  mpt2eq123  5584  mpt2eq123dva  5586  mpt2eq3dva  5589  nfmpt21  5591  nfmpt22  5592  nfmpt2  5593  mpt20  5594  cbvmpt2x  5602  mpt2v  5614  mpt2mptx  5615  resmpt2  5619  mpt2fun  5623  mpt22eqb  5630  rnmpt2  5631  reldmmpt2  5632  ovmpt4g  5643  elmpt2cl  5718  fmpt2x  5846  f1od2  5876  tposmpt2  5919  erovlem  6221  xpcomco  6323  dfplpq2  6544  dfmpq2  6545