df-mpo

Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x , y (in A X. B ) to C ( x , y ) ". An extension of df-mpt for two arguments. (Contributed by NM, 17-Feb-2008)

		Ref	Expression
	Assertion	df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$setvar x$
1		cA	$class A$
2		vy	$setvar y$
3		cB	$class B$
4		cC	$class C$
5	0 2 1 3 4	cmpo	$class (x \in A, y \in B ⟼ C)$
6		vz	$setvar z$
7	0	cv	$setvar x$
8	7 1	wcel	$wff x \in A$
9	2	cv	$setvar y$
10	9 3	wcel	$wff y \in B$
11	8 10	wa	$wff (x \in A \land y \in B)$
12	6	cv	$setvar z$
13	12 4	wceq	$wff z = C$
14	11 13	wa	$wff ((x \in A \land y \in B) \land z = C)$
15	14 0 2 6	coprab	$class \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
16	5 15	wceq	$wff (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$

Metamath Proof Explorer

Definition df-mpo

Detailed syntax breakdown