Definition df-opab 5154

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 5513 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 7984. An example is given by ex-opab 30407. (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 5153	. 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 4582	. . . . . . 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 2709	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1541	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5155  opabbid  5156  opabbidv  5157  nfopabd  5159  nfopab1  5161  nfopab2  5162  cbvopab  5163  cbvopabv  5164  cbvopab1  5165  cbvopab1g  5166  cbvopab2  5167  cbvopab1s  5168  cbvopab1v  5169  cbvopab2v  5170  unopab  5171  opabidw  5464  opabid  5465  elopabw  5466  ssopab2  5486  iunopab  5499  dfid2  5513  dfid3  5514  elxpi  5638  opabssxpd  5663  rabxp  5664  csbxp  5716  relopabi  5762  relopabiALT  5763  cnv0  6087  dfoprab2  7404  dmoprab  7449  dfopab2  7984  brdom7disj  10419  brdom6disj  10420  opabssi  32591  cbvopab1davw  36297  cbvopab2davw  36298  cbvopabdavw  36299  bj-dfid2ALT  37098  rnxrn  38429  dropab1  44478  dropab2  44479  csbxpgVD  44925  relopabVD  44932