Definition df-opab 2098

Description: Define class abstractions of ordered pairs. Definition 3.3 of [Monk1] p. 34. Normally x and y are distinct, although the definition doesn't strictly require it.

Assertion

Ref	Expression
df-opab	⊢ {⟨x, y⟩∣φ} = {z∣∃x∃y(z = ⟨x, y⟩ ∧ φ)}

Distinct variable group(s):   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 2055	. 2 class {⟨x, y⟩∣φ}
5		vz	. . . . . . . 8 set z
6	5	cv 1089	. . . . . . 7 class z
7	2	cv 1089	. . . . . . . 8 class x
8	3	cv 1089	. . . . . . . 8 class y
9	7, 8	cop 1810	. . . . . . 7 class ⟨x, y⟩
10	6, 9	wceq 1091	. . . . . 6 wff z = ⟨x, y⟩
11	10, 1	wa 196	. . . . 5 wff (z = ⟨x, y⟩ ∧ φ)
12	11, 3	wex 678	. . . 4 wff ∃y(z = ⟨x, y⟩ ∧ φ)
13	12, 2	wex 678	. . 3 wff ∃x∃y(z = ⟨x, y⟩ ∧ φ)
14	13, 5	cab 1090	. 2 class {z∣∃x∃y(z = ⟨x, y⟩ ∧ φ)}
15	4, 14	wceq 1091	1 wff {⟨x, y⟩∣φ} = {z∣∃x∃y(z = ⟨x, y⟩ ∧ φ)}

This definition is referenced by:  opabid 2099  opabss 2100  biopabd 2101  cbvopab 2104  cbvopab1 2106  cbvopab1s 2107  cbvopab1v 2108  cbvopab2v 2109  elopab 2110  hbopab1 2112  hbopab2 2113  ssopab2 2119  unopab 2121  rdglem2 2976  dfoprab2 3021  dmoprab 3031

metamath.org