df-oprab - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-oprab 3951

Description: Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally

, and

are distinct, although the definition doesn't strictly require it. See df-opr 3950 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by oprabval2 4013.

**Assertion**
Ref	Expression
df-oprab	$/\$

Distinct variable groups:

**Detailed syntax breakdown of Definition df-oprab**
Step	Hyp	Ref	Expression
1		wph	. . 3
2		vx	. . 3
3		vy	. . 3
4		vz	. . 3
5	1, 2, 3, 4	copab2 3949	. 2
6		vw	. . . . . . . . 9
7	6	cv 952	. . . . . . . 8
8	2	cv 952	. . . . . . . . . 10
9	3	cv 952	. . . . . . . . . 10
10	8, 9	cop 2401	. . . . . . . . 9
11	4	cv 952	. . . . . . . . 9
12	10, 11	cop 2401	. . . . . . . 8
13	7, 12	wceq 953	. . . . . . 7
14	13, 1	wa 223	. . . . . 6 $/\$
15	14, 4	wex 977	. . . . 5 $/\$
16	15, 3	wex 977	. . . 4 $/\$
17	16, 2	wex 977	. . 3 $/\$
18	17, 6	cab 1456	. 2 $/\$
19	5, 18	wceq 953	1 $/\$

Colors of variables: wff set class

This definition is referenced by: dfoprab2 3976 hboprab1 3978 hboprab2 3979 cbvoprab12 3983 eloprabg 3992