Definition df-mpt 5652

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 SF, 5-Jan-2015.)

Assertion

Ref	Expression
df-mpt	⊢ (x ∈ A ↦ B) = {⟨x, y⟩ ∣ (x ∈ 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 5651	. 2 class (x ∈ A ↦ B)
5	1	cv 1641	. . . . 5 class x
6	5, 2	wcel 1710	. . . 4 wff x ∈ A
7		vy	. . . . . 6 setvar y
8	7	cv 1641	. . . . 5 class y
9	8, 3	wceq 1642	. . . 4 wff y = B
10	6, 9	wa 358	. . 3 wff (x ∈ A ∧ y = B)
11	10, 1, 7	copab 4622	. 2 class {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)}
12	4, 11	wceq 1642	1 wff (x ∈ A ↦ B) = {⟨x, y⟩ ∣ (x ∈ A ∧ y = B)}

This definition is referenced by:  mpteq12f  5655  nfmpt  5671  nfmpt1  5672  cbvmpt  5676  fconstmpt  5681  mptpreima  5682  dmmpt  5683  dmmptss  5685  rnmpt  5686  funmpt  5687  mptfng  5688  resmpt  5696  fvmptg  5698  dffn5v  5706  mpt2mptx  5708  mptv  5718  mptresid  5720  f1od  5726  releqmpt  5808  enmap2lem1  6063  enmap1lem1  6069  scancan  6331