Definition df-opab

Description: Define the class abstraction of a collection of ordered pairs. Definition 3.3 of Monk1 p. 34. Usually x and y are distinct, although the definition does not require it (see dfid2 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also called "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 . An example is given by ex-opab . (Contributed by NM, 4-Jul-1994)

	Ref	Expression
Assertion	df-opab	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		vy	|- y
2		wph	|- ph
3	2 0 1	copab	|- { <. x , y >. | ph }
4		vz	|- z
5	4	cv	|- z
6	0	cv	|- x
7	1	cv	|- y
8	6 7	cop	|- <. x , y >.
9	5 8	wceq	|- z = <. x , y >.
10	9 2	wa	|- ( z = <. x , y >. /\ ph )
11	10 1	wex	|- E. y ( z = <. x , y >. /\ ph )
12	11 0	wex	|- E. x E. y ( z = <. x , y >. /\ ph )
13	12 4	cab	|- { z | E. x E. y ( z = <. x , y >. /\ ph ) }
14	3 13	wceq	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }