Definition df-mpt 5006

Description: Define maps-to notation for defining a function via a rule. Read as "the function defined by the map from x (in A) to B(x)." The class expression B is the value of the function at x and normally contains the variable x. An example is the square function for complex numbers, (x e. CC |-> (x^2). Similar to the definition of mapping in [ChoquetDD] p. 2.

Assertion

Ref	Expression
df-mpt	|- (x e. A |-> B) = {<.x, y>. | (x e. A /\ y = B)}

Distinct variable groups:   x,y   y,A   y,B

Detailed syntax breakdown of Definition df-mpt

Step	Hyp	Ref	Expression
1		vx	. . 3 set x
2		cA	. . 3 class A
3		cB	. . 3 class B
4	1, 2, 3	cmpt 5004	. 2 class (x e. A |-> B)
5	1	cv 1297	. . . . 5 class x
6	5, 2	wcel 1300	. . . 4 wff x e. A
7		vy	. . . . . 6 set y
8	7	cv 1297	. . . . 5 class y
9	8, 3	wceq 1298	. . . 4 wff y = B
10	6, 9	wa 240	. . 3 wff (x e. A /\ y = B)
11	10, 1, 7	copab 3395	. 2 class {<.x, y>. | (x e. A /\ y = B)}
12	4, 11	wceq 1298	1 wff (x e. A |-> B) = {<.x, y>. | (x e. A /\ y = B)}

This definition is referenced by:  mpteq12dv 5008  hbmpt1 5010  cbvmpt 5011  mptexg 5012  fvmptg 5014  dfmpt 5073  frsucmpt 5163  mptfn 10162  rnmpt 10163  mpteqi 13838  fvopab2b 14476  cmpbvb 14477  fopab2ga 14478  fopab2a 14479  cmpfun 14480  cmpran 14483  cmprtr 14760  trhom 14983  trnij 15015  cnvtr 15016  supbrr 15048

Copyright terms: Public domain