df-opab - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Definition df-opab 2741

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 doesn't strictly require it (see dfid2 2915 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 4173.

**Assertion**
Ref	Expression
df-opab	⊢ {x, y∣φ} = {z∣∃x∃y(z = x, y ⋀ φ)}

Distinct variable groups: x,z y,z φ,z

**Detailed syntax breakdown of Definition df-opab**
Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 set x
3		vy	. . 3 set y
4	1, 2, 3	copab 2740	. 2 class {x, y∣φ}
5		vz	. . . . . . . 8 set z
6	5	cv 991	. . . . . . 7 class z
7	2	cv 991	. . . . . . . 8 class x
8	3	cv 991	. . . . . . . 8 class y
9	7, 8	cop 2469	. . . . . . 7 class x, y
10	6, 9	wceq 992	. . . . . 6 wff z = x, y
11	10, 1	wa 221	. . . . 5 wff (z = x, y ⋀ φ)
12	11, 3	wex 1016	. . . 4 wff ∃y(z = x, y ⋀ φ)
13	12, 2	wex 1016	. . 3 wff ∃x∃y(z = x, y ⋀ φ)
14	13, 5	cab 1505	. 2 class {z∣∃x∃y(z = x, y ⋀ φ)}
15	4, 14	wceq 992	1 wff {x, y∣φ} = {z∣∃x∃y(z = x, y ⋀ φ)}

Colors of variables: wff set class

This definition is referenced by: opabss 2742 opabbid 2743 cbvopab 2746 cbvopab1 2748 cbvopab1s 2749 cbvopab2v 2751 csbopabg 2752 unopab 2753 opabid 2887 elopab 2888 hbopab1 2890 hbopab2 2891 ssopab2 2900 dfid3 2914 dfoprab2 4050 dmoprab 4062 dfopab2 4173 rdglem2 4239 brdom7disj 4950 brdom6disj 4951 nvvcop 8460 oprabopabf 11807