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	$⊢ (x \in A ⟼ B) = \{⟨x, y⟩ \| (x \in A \land y = B)\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$setvar x$
1		cA	$class A$
2		cB	$class B$
3	0 1 2	cmpt	$class (x \in A ⟼ B)$
4		vy	$setvar y$
5	0	cv	$setvar x$
6	5 1	wcel	$wff x \in A$
7	4	cv	$setvar y$
8	7 2	wceq	$wff y = B$
9	6 8	wa	$wff (x \in A \land y = B)$
10	9 0 4	copab	$class \{⟨x, y⟩ \| (x \in A \land y = B)\}$
11	3 10	wceq	$wff (x \in A ⟼ B) = \{⟨x, y⟩ \| (x \in A \land y = B)\}$