Definition df-mpt 4070

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 4068	. 2 class (x e. A |-> B)
5	1	cv 954	. . . . 5 class x
6	5, 2	wcel 957	. . . 4 wff x e. A
7		vy	. . . . . 6 set y
8	7	cv 954	. . . . 5 class y
9	8, 3	wceq 955	. . . 4 wff y = B
10	6, 9	wa 223	. . 3 wff (x e. A /\ y = B)
11	10, 1, 7	copab 2663	. 2 class {<.x, y>. | (x e. A /\ y = B)}
12	4, 11	wceq 955	1 wff (x e. A |-> B) = {<.x, y>. | (x e. A /\ y = B)}

This definition is referenced by:  mptg 4072  hbcmpt 10451  fvopab2a 10452  cmpbva 10453  fopab2ga 10454  fopab2a 10455  cmpfun 10456  cmpran 10458  trnij 10588  cnvtr 10589

Copyright terms: Public domain