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

Definition df-mpt2 5460
 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 3811 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 5457 . 2 class (x A, y B𝐶)
71cv 1241 . . . . . 6 class x
87, 3wcel 1390 . . . . 5 wff x A
92cv 1241 . . . . . 6 class y
109, 4wcel 1390 . . . . 5 wff y B
118, 10wa 97 . . . 4 wff (x A y B)
12 vz . . . . . 6 setvar z
1312cv 1241 . . . . 5 class z
1413, 5wceq 1242 . . . 4 wff z = 𝐶
1511, 14wa 97 . . 3 wff ((x A y B) z = 𝐶)
1615, 1, 2, 12coprab 5456 . 2 class {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) z = 𝐶)}
176, 16wceq 1242 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  5506  mpt2eq123dva  5508  mpt2eq3dva  5511  nfmpt21  5513  nfmpt22  5514  nfmpt2  5515  mpt20  5516  cbvmpt2x  5524  mpt2v  5536  mpt2mptx  5537  resmpt2  5541  mpt2fun  5545  mpt22eqb  5552  rnmpt2  5553  reldmmpt2  5554  ovmpt4g  5565  elmpt2cl  5640  fmpt2x  5768  tposmpt2  5837  erovlem  6134  xpcomco  6236  dfplpq2  6338  dfmpq2  6339
 Copyright terms: Public domain W3C validator