Definition df-mpt2 5517

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 3820 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 5514	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1242	. . . . . 6 class 𝑥
8	7, 3	wcel 1393	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1242	. . . . . 6 class 𝑦
10	9, 4	wcel 1393	. . . . 5 wff 𝑦 ∈ 𝐵
11	8, 10	wa 97	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
12		vz	. . . . . 6 setvar 𝑧
13	12	cv 1242	. . . . 5 class 𝑧
14	13, 5	wceq 1243	. . . 4 wff 𝑧 = 𝐶
15	11, 14	wa 97	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
16	15, 1, 2, 12	coprab 5513	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1243	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is referenced by:  mpt2eq123  5564  mpt2eq123dva  5566  mpt2eq3dva  5569  nfmpt21  5571  nfmpt22  5572  nfmpt2  5573  mpt20  5574  cbvmpt2x  5582  mpt2v  5594  mpt2mptx  5595  resmpt2  5599  mpt2fun  5603  mpt22eqb  5610  rnmpt2  5611  reldmmpt2  5612  ovmpt4g  5623  elmpt2cl  5698  fmpt2x  5826  tposmpt2  5896  erovlem  6198  xpcomco  6300  dfplpq2  6452  dfmpq2  6453