Definition df-mpt 3811

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. Similar to the definition of mapping in [ChoquetDD] p. 2. (Contributed by NM, 17-Feb-2008.)

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

Allowed substitution hints:   A(x)   B(x)

Detailed syntax breakdown of Definition df-mpt

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar x
2		cA	. . 3 class A
3		cB	. . 3 class B
4	1, 2, 3	cmpt 3809	. 2 class (x e. A |-> B)
5	1	cv 1241	. . . . 5 class x
6	5, 2	wcel 1390	. . . 4 wff x e. A
7		vy	. . . . . 6 setvar y
8	7	cv 1241	. . . . 5 class y
9	8, 3	wceq 1242	. . . 4 wff y = B
10	6, 9	wa 97	. . 3 wff (x e. A /\ y = B)
11	10, 1, 7	copab 3808	. 2 class { <.x , y >. | (x e. A /\ y = B) }
12	4, 11	wceq 1242	1 wff (x e. A |-> B) = { <.x , y >. | (x e. A /\ y = B) }

This definition is referenced by:  mpteq12f  3828  nfmpt  3840  nfmpt1  3841  cbvmpt  3842  mptv  3844  fconstmpt  4330  rnmpt  4525  resmpt  4599  mptresid  4603  mptpreima  4757  funmpt  4881  dfmpt3  4964  mptfng  4967  mptun  4972  dffn5im  5162  fvmptss2  5190  fvmptg  5191  fndmin  5217  f1ompt  5263  fmptco  5273  mpt2mptx  5537  f1ocnvd  5644  dftpos4  5819