Definition df-mpt2 6655

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 4730 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 6652	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1482	. . . . . 6 class 𝑥
8	7, 3	wcel 1990	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1482	. . . . . 6 class 𝑦
10	9, 4	wcel 1990	. . . . 5 wff 𝑦 ∈ 𝐵
11	8, 10	wa 384	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
12		vz	. . . . . 6 setvar 𝑧
13	12	cv 1482	. . . . 5 class 𝑧
14	13, 5	wceq 1483	. . . 4 wff 𝑧 = 𝐶
15	11, 14	wa 384	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
16	15, 1, 2, 12	coprab 6651	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1483	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is referenced by:  mpt2eq123  6714  mpt2eq123dva  6716  mpt2eq3dva  6719  nfmpt21  6722  nfmpt22  6723  nfmpt2  6724  mpt20  6725  cbvmpt2x  6733  mpt2v  6750  mpt2mptx  6751  resmpt2  6758  mpt2fun  6762  mpt22eqb  6769  rnmpt2  6770  reldmmpt2  6771  elrnmpt2res  6774  ovmpt4g  6783  mpt2ndm0  6875  elmpt2cl  6876  fmpt2x  7236  bropopvvv  7255  bropfvvvv  7257  tposmpt2  7389  erovlem  7843  xpcomco  8050  omxpenlem  8061  cpnnen  14958  mpt2mptxf  29477  df1stres  29481  df2ndres  29482  f1od2  29499  sxbrsigalem5  30350  dmscut  31918  bj-dfmpt2a  33071  csbmpt22g  33177  uncf  33388  unccur  33392  mpt2bi123f  33971  cbvmpt22  39277  cbvmpt21  39278  mpt2mptx2  42113  cbvmpt2x2  42114