This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-mpt

Description: Define maps-to notation for defining a function via a rule. Read as "the function which maps 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. (Contributed by NM, 17-Feb-2008)

		Ref	Expression
	Assertion	df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		cA	⊢ 𝐴
2		cB	⊢ 𝐵
3	0 1 2	cmpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4		vy	⊢ 𝑦
5	0	cv	⊢ 𝑥
6	5 1	wcel	⊢ 𝑥 ∈ 𝐴
7	4	cv	⊢ 𝑦
8	7 2	wceq	⊢ 𝑦 = 𝐵
9	6 8	wa	⊢ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 )
10	9 0 4	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
11	3 10	wceq	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }