Definition df-opab 5163

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 5531 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 8008. An example is given by ex-opab 30525. (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 5162	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1541	. . . . . . 7 class 𝑧
7	2	cv 1541	. . . . . . . 8 class 𝑥
8	3	cv 1541	. . . . . . . 8 class 𝑦
9	7, 8	cop 4588	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1542	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 395	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1781	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1781	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2715	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1542	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5164  opabbid  5165  opabbidv  5166  nfopabd  5168  nfopab1  5170  nfopab2  5171  cbvopab  5172  cbvopabv  5173  cbvopab1  5174  cbvopab1g  5175  cbvopab2  5176  cbvopab1s  5177  cbvopab1v  5178  cbvopab2v  5179  unopab  5180  opabidw  5482  opabid  5483  elopabw  5484  ssopab2  5504  iunopab  5517  dfid2  5531  dfid3  5532  elxpi  5656  opabssxpd  5681  rabxp  5682  csbxp  5735  relopabi  5781  relopabiALT  5782  cnv0OLD  6108  dfoprab2  7428  dmoprab  7473  dfopab2  8008  brdom7disj  10455  brdom6disj  10456  opabssi  32709  cbvopab1davw  36486  cbvopab2davw  36487  cbvopabdavw  36488  bj-dfid2ALT  37340  rnxrn  38701  dropab1  44831  dropab2  44832  csbxpgVD  45278  relopabVD  45285