ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-mpt2 GIF version

Definition df-mpt2 5545
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 3848 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 5542 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1258 . . . . . 6 class 𝑥
87, 3wcel 1409 . . . . 5 wff 𝑥𝐴
92cv 1258 . . . . . 6 class 𝑦
109, 4wcel 1409 . . . . 5 wff 𝑦𝐵
118, 10wa 101 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1258 . . . . 5 class 𝑧
1413, 5wceq 1259 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 101 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 5541 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1259 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff set class
This definition is referenced by:  mpt2eq123  5592  mpt2eq123dva  5594  mpt2eq3dva  5597  nfmpt21  5599  nfmpt22  5600  nfmpt2  5601  mpt20  5602  cbvmpt2x  5610  mpt2v  5622  mpt2mptx  5623  resmpt2  5627  mpt2fun  5631  mpt22eqb  5638  rnmpt2  5639  reldmmpt2  5640  ovmpt4g  5651  elmpt2cl  5726  fmpt2x  5854  f1od2  5884  tposmpt2  5927  erovlem  6229  xpcomco  6331  dfplpq2  6510  dfmpq2  6511
  Copyright terms: Public domain W3C validator