Definition df-opab 5158

Description: Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually 𝑥 and 𝑦 are distinct, although the definition does not require it (see dfid2 5520 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 7994. An example is given by ex-opab 30394. (Contributed by NM, 4-Jul-1994.)

Assertion

Ref	Expression
df-opab	⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

Distinct variable groups:   𝑥,𝑧   𝑦,𝑧   𝜑,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦)

Detailed syntax breakdown of Definition df-opab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4	1, 2, 3	copab 5157	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1539	. . . . . . 7 class 𝑧
7	2	cv 1539	. . . . . . . 8 class 𝑥
8	3	cv 1539	. . . . . . . 8 class 𝑦
9	7, 8	cop 4585	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1540	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 395	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1779	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1779	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2707	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1540	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5159  opabbid  5160  opabbidv  5161  nfopabd  5163  nfopab1  5165  nfopab2  5166  cbvopab  5167  cbvopabv  5168  cbvopab1  5169  cbvopab1g  5170  cbvopab2  5171  cbvopab1s  5172  cbvopab1v  5173  cbvopab2v  5174  unopab  5175  opabidw  5471  opabid  5472  elopabw  5473  ssopab2  5493  iunopab  5506  dfid2  5520  dfid3  5521  elxpi  5645  opabssxpd  5670  rabxp  5671  csbxp  5723  relopabi  5769  relopabiALT  5770  cnv0  6093  dfoprab2  7411  dmoprab  7456  dfopab2  7994  brdom7disj  10444  brdom6disj  10445  opabssi  32574  cbvopab1davw  36237  cbvopab2davw  36238  cbvopabdavw  36239  bj-dfid2ALT  37038  rnxrn  38369  dropab1  44420  dropab2  44421  csbxpgVD  44867  relopabVD  44874