df-oprab - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-oprab 4887

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 4886 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 4957.

**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 4885	. 2
6		vw	. . . . . . . . 9
7	6	cv 1297	. . . . . . . 8
8	2	cv 1297	. . . . . . . . . 10
9	3	cv 1297	. . . . . . . . . 10
10	8, 9	cop 3046	. . . . . . . . 9
11	4	cv 1297	. . . . . . . . 9
12	10, 11	cop 3046	. . . . . . . 8
13	7, 12	wceq 1298	. . . . . . 7
14	13, 1	wa 240	. . . . . 6 $/\$
15	14, 4	wex 1326	. . . . 5 $/\$
16	15, 3	wex 1326	. . . 4 $/\$
17	16, 2	wex 1326	. . 3 $/\$
18	17, 6	cab 1871	. 2 $/\$
19	5, 18	wceq 1298	1 $/\$

Colors of variables: wff set class

This definition is referenced by: dfoprab2 4917 hboprab1 4919 hboprab2 4920 cbvoprab1OLD 4925 cbvoprab12OLD 4927 eloprabg 4936 oprabopabf 10157 cbvoprab2 15708 oprabrexex2 15709