Definition df-mpt 4061

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 4059	. 2 class ( x e. A |-> B )
5	1	cv 1352	. . . . 5 class x
6	5, 2	wcel 2146	. . . 4 wff x e. A
7		vy	. . . . . 6 setvar y
8	7	cv 1352	. . . . 5 class y
9	8, 3	wceq 1353	. . . 4 wff y = B
10	6, 9	wa 104	. . 3 wff ( x e. A /\ y = B )
11	10, 1, 7	copab 4058	. 2 class { <. x , y >. | ( x e. A /\ y = B ) }
12	4, 11	wceq 1353	1 wff ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }

This definition is referenced by:  mpteq12f  4078  nfmpt  4090  nfmpt1  4091  cbvmptf  4092  cbvmpt  4093  mptv  4095  fconstmpt  4667  mptrel  4748  rnmpt  4868  resmpt  4948  mptresid  4954  mptcnv  5023  mptpreima  5114  funmpt  5246  dfmpt3  5330  mptfng  5333  mptun  5339  dffn5im  5553  fvmptss2  5583  fvmptg  5584  fndmin  5615  f1ompt  5659  fmptco  5674  mpomptx  5956  f1ocnvd  6063  f1od2  6226  dftpos4  6254  mapsncnv  6685