Definition df-mpt 5653

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 5652	. 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 4623	. 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  5656  nfmpt  5672  nfmpt1  5673  cbvmpt  5677  fconstmpt  5682  mptpreima  5683  dmmpt  5684  dmmptss  5686  rnmpt  5687  funmpt  5688  mptfng  5689  resmpt  5697  fvmptg  5699  dffn5v  5707  mpt2mptx  5709  mptv  5719  mptresid  5721  f1od  5727  releqmpt  5809  enmap2lem1  6064  enmap1lem1  6070  scancan  6332