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 6695
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 4763 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 6692 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1522 . . . . . 6 class 𝑥
87, 3wcel 2030 . . . . 5 wff 𝑥𝐴
92cv 1522 . . . . . 6 class 𝑦
109, 4wcel 2030 . . . . 5 wff 𝑦𝐵
118, 10wa 383 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1522 . . . . 5 class 𝑧
1413, 5wceq 1523 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 383 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 6691 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1523 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff setvar class
This definition is referenced by:  mpt2eq123  6756  mpt2eq123dva  6758  mpt2eq3dva  6761  nfmpt21  6764  nfmpt22  6765  nfmpt2  6766  mpt20  6767  cbvmpt2x  6775  mpt2v  6792  mpt2mptx  6793  resmpt2  6800  mpt2fun  6804  mpt22eqb  6811  rnmpt2  6812  reldmmpt2  6813  elrnmpt2res  6816  ovmpt4g  6825  mpt2ndm0  6917  elmpt2cl  6918  fmpt2x  7281  bropopvvv  7300  bropfvvvv  7302  tposmpt2  7434  erovlem  7886  xpcomco  8091  omxpenlem  8102  cpnnen  15002  mpt2mptxf  29605  df1stres  29609  df2ndres  29610  f1od2  29627  sxbrsigalem5  30478  dmscut  32043  bj-dfmpt2a  33196  csbmpt22g  33307  uncf  33518  unccur  33522  mpt2bi123f  34101  cbvmpt22  39591  cbvmpt21  39592  mpt2mptx2  42438  cbvmpt2x2  42439
  Copyright terms: Public domain W3C validator