Definition df-opab 5167

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 5544 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 8046. An example is given by ex-opab 30966. (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 5166	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1569	. . . . . . 7 class 𝑧
7	2	cv 1569	. . . . . . . 8 class 𝑥
8	3	cv 1569	. . . . . . . 8 class 𝑦
9	7, 8	cop 4589	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1570	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 401	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1812	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1812	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2738	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1570	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is used by:  opabss  5168  opabbid  5169  opabbidv  5170  nfopabd  5172  nfopab1  5174  nfopab2  5175  cbvopab  5176  cbvopabv  5177  cbvopab1  5178  cbvopab1g  5179  cbvopab2  5180  cbvopab1s  5181  cbvopab1v  5182  cbvopab2v  5183  unopab  5184  opabidw  5494  opabid  5495  elopabw  5496  ssopab2  5517  iunopab  5530  dfid2  5544  dfid3  5545  elxpi  5669  opabssxpd  5694  rabxp  5695  csbxp  5748  relopabi  5796  relopabiALT  5797  cnv0OLD  5858  dfoprab2  7466  dmoprab  7511  dfopab2  8046  brdom7disj  10581  brdom6disj  10582  opabssi  33140  cbvopab1davw  36975  cbvopab2davw  36976  cbvopabdavw  36977  bj-dfid2ALT  37900  rnxrn  39273  dropab1  45374  dropab2  45375  csbxpgVD  45820  relopabVD  45827