Definition df-opab 5156

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 5516 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 7990. An example is given by ex-opab 30414. (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 5155	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1540	. . . . . . 7 class 𝑧
7	2	cv 1540	. . . . . . . 8 class 𝑥
8	3	cv 1540	. . . . . . . 8 class 𝑦
9	7, 8	cop 4581	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1541	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 395	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1780	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1780	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2711	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1541	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5157  opabbid  5158  opabbidv  5159  nfopabd  5161  nfopab1  5163  nfopab2  5164  cbvopab  5165  cbvopabv  5166  cbvopab1  5167  cbvopab1g  5168  cbvopab2  5169  cbvopab1s  5170  cbvopab1v  5171  cbvopab2v  5172  unopab  5173  opabidw  5467  opabid  5468  elopabw  5469  ssopab2  5489  iunopab  5502  dfid2  5516  dfid3  5517  elxpi  5641  opabssxpd  5666  rabxp  5667  csbxp  5720  relopabi  5766  relopabiALT  5767  cnv0OLD  6092  dfoprab2  7410  dmoprab  7455  dfopab2  7990  brdom7disj  10429  brdom6disj  10430  opabssi  32598  cbvopab1davw  36329  cbvopab2davw  36330  cbvopabdavw  36331  bj-dfid2ALT  37130  rnxrn  38465  dropab1  44563  dropab2  44564  csbxpgVD  45010  relopabVD  45017