Definition df-opab 5162

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 5522 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 7998. An example is given by ex-opab 30511. (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 5161	. 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 4587	. . . . . . 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  5163  opabbid  5164  opabbidv  5165  nfopabd  5167  nfopab1  5169  nfopab2  5170  cbvopab  5171  cbvopabv  5172  cbvopab1  5173  cbvopab1g  5174  cbvopab2  5175  cbvopab1s  5176  cbvopab1v  5177  cbvopab2v  5178  unopab  5179  opabidw  5473  opabid  5474  elopabw  5475  ssopab2  5495  iunopab  5508  dfid2  5522  dfid3  5523  elxpi  5647  opabssxpd  5672  rabxp  5673  csbxp  5726  relopabi  5772  relopabiALT  5773  cnv0OLD  6099  dfoprab2  7418  dmoprab  7463  dfopab2  7998  brdom7disj  10445  brdom6disj  10446  opabssi  32694  cbvopab1davw  36460  cbvopab2davw  36461  cbvopabdavw  36462  bj-dfid2ALT  37268  rnxrn  38624  dropab1  44754  dropab2  44755  csbxpgVD  45201  relopabVD  45208