MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mpt2 Structured version   Visualization version   GIF version

Definition df-mpt2 6620
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 4685 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
StepHypRef Expression
1 vx . . 3 setvar 𝑥
2 vy . . 3 setvar 𝑦
3 cA . . 3 class 𝐴
4 cB . . 3 class 𝐵
5 cC . . 3 class 𝐶
61, 2, 3, 4, 5cmpt2 6617 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1479 . . . . . 6 class 𝑥
87, 3wcel 1987 . . . . 5 wff 𝑥𝐴
92cv 1479 . . . . . 6 class 𝑦
109, 4wcel 1987 . . . . 5 wff 𝑦𝐵
118, 10wa 384 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1479 . . . . 5 class 𝑧
1413, 5wceq 1480 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 384 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 6616 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1480 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff setvar class
This definition is referenced by:  mpt2eq123  6679  mpt2eq123dva  6681  mpt2eq3dva  6684  nfmpt21  6687  nfmpt22  6688  nfmpt2  6689  mpt20  6690  cbvmpt2x  6698  mpt2v  6715  mpt2mptx  6716  resmpt2  6723  mpt2fun  6727  mpt22eqb  6734  rnmpt2  6735  reldmmpt2  6736  elrnmpt2res  6739  ovmpt4g  6748  mpt2ndm0  6840  elmpt2cl  6841  fmpt2x  7196  bropopvvv  7215  bropfvvvv  7217  tposmpt2  7349  erovlem  7803  xpcomco  8010  omxpenlem  8021  cpnnen  14902  mpt2mptxf  29361  df1stres  29365  df2ndres  29366  f1od2  29383  sxbrsigalem5  30173  bj-dfmpt2a  32747  csbmpt22g  32848  uncf  33059  unccur  33063  mpt2bi123f  33642  cbvmpt22  38799  cbvmpt21  38800  mpt2mptx2  41431  cbvmpt2x2  41432
  Copyright terms: Public domain W3C validator