Definition df-opab 5206

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 5580 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 8077. An example is given by ex-opab 30451. (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 5205	. 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 4632	. . . . . . 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 2714	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1540	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5207  opabbid  5208  opabbidv  5209  nfopabd  5211  nfopab1  5213  nfopab2  5214  cbvopab  5215  cbvopabv  5216  cbvopab1  5217  cbvopab1g  5218  cbvopab2  5219  cbvopab1s  5220  cbvopab1v  5221  cbvopab2v  5223  unopab  5224  opabidw  5529  opabid  5530  elopabw  5531  ssopab2  5551  iunopab  5564  iunopabOLD  5565  dfid2  5580  dfid3  5581  elxpi  5707  opabssxpd  5732  rabxp  5733  csbxp  5785  ssrelOLD  5793  relopabi  5832  relopabiALT  5833  cnv0  6160  dfoprab2  7491  dmoprab  7536  dfopab2  8077  brdom7disj  10571  brdom6disj  10572  opabssi  32625  cbvopab1davw  36265  cbvopab2davw  36266  cbvopabdavw  36267  bj-dfid2ALT  37066  rnxrn  38399  dropab1  44466  dropab2  44467  csbxpgVD  44914  relopabVD  44921