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

Definition df-mpt2 5432
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 3786 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 5429 . 2 class (x A, y B𝐶)
71cv 1225 . . . . . 6 class x
87, 3wcel 1369 . . . . 5 wff x A
92cv 1225 . . . . . 6 class y
109, 4wcel 1369 . . . . 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 5428 . 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  5478  mpt2eq123dva  5480  mpt2eq3dva  5483  nfmpt21  5485  nfmpt22  5486  nfmpt2  5487  mpt20  5488  cbvmpt2x  5496  mpt2v  5508  mpt2mptx  5509  resmpt2  5513  mpt2fun  5517  mpt22eqb  5524  rnmpt2  5525  reldmmpt2  5526  ovmpt4g  5537  elmpt2cl  5612  fmpt2x  5740  tposmpt2  5809  erovlem  6100  dfplpq2  6202  dfmpq2  6203
  Copyright terms: Public domain W3C validator