Definition df-mpt2 5495

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 3817 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 5492	. 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 5491	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1243	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is referenced by:  mpt2eq123  5542  mpt2eq123dva  5544  mpt2eq3dva  5547  nfmpt21  5549  nfmpt22  5550  nfmpt2  5551  mpt20  5552  cbvmpt2x  5560  mpt2v  5572  mpt2mptx  5573  resmpt2  5577  mpt2fun  5581  mpt22eqb  5588  rnmpt2  5589  reldmmpt2  5590  ovmpt4g  5601  elmpt2cl  5676  fmpt2x  5804  tposmpt2  5874  erovlem  6176  xpcomco  6278  dfplpq2  6424  dfmpq2  6425