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

Definition df-mpt2 5437
Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x, y (in A × B) to B(x, y)." An extension of df-mpt 3790 for two arguments. (Contributed by NM, 17-Feb-2008.)
Assertion
Ref Expression
df-mpt2 (x A, y B𝐶) = {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) z = 𝐶)}
Distinct variable groups:   x,z   y,z   z,A   z,B   z,𝐶
Allowed substitution hints:   A(x,y)   B(x,y)   𝐶(x,y)

Detailed syntax breakdown of Definition df-mpt2
StepHypRef Expression
1 vx . . 3 setvar x
2 vy . . 3 setvar y
3 cA . . 3 class A
4 cB . . 3 class B
5 cC . . 3 class 𝐶
61, 2, 3, 4, 5cmpt2 5434 . 2 class (x A, y B𝐶)
71cv 1225 . . . . . 6 class x
87, 3wcel 1370 . . . . 5 wff x A
92cv 1225 . . . . . 6 class y
109, 4wcel 1370 . . . . 5 wff y B
118, 10wa 97 . . . 4 wff (x A y B)
12 vz . . . . . 6 setvar z
1312cv 1225 . . . . 5 class z
1413, 5wceq 1226 . . . 4 wff z = 𝐶
1511, 14wa 97 . . 3 wff ((x A y B) z = 𝐶)
1615, 1, 2, 12coprab 5433 . 2 class {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) z = 𝐶)}
176, 16wceq 1226 1 wff (x A, y B𝐶) = {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) z = 𝐶)}
Colors of variables: wff set class
This definition is referenced by:  mpt2eq123  5483  mpt2eq123dva  5485  mpt2eq3dva  5488  nfmpt21  5490  nfmpt22  5491  nfmpt2  5492  mpt20  5493  cbvmpt2x  5501  mpt2v  5513  mpt2mptx  5514  resmpt2  5518  mpt2fun  5522  mpt22eqb  5529  rnmpt2  5530  reldmmpt2  5531  ovmpt4g  5542  elmpt2cl  5617  fmpt2x  5745  tposmpt2  5814  erovlem  6105  dfplpq2  6207  dfmpq2  6208
  Copyright terms: Public domain W3C validator