Definition df-opab 5173

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 5538 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 7989. An example is given by ex-opab 29439. (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 5172	. 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 4597	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1541	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 396	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1781	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1781	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2708	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1541	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5174  opabbid  5175  opabbidv  5176  nfopabd  5178  nfopab1  5180  nfopab2  5181  cbvopab  5182  cbvopabv  5183  cbvopab1  5185  cbvopab1g  5186  cbvopab2  5187  cbvopab1s  5188  cbvopab1v  5189  cbvopab2v  5191  unopab  5192  opabidw  5486  opabid  5487  elopabw  5488  ssopab2  5508  iunopab  5521  iunopabOLD  5522  dfid2  5538  dfid3  5539  elxpi  5660  opabssxpd  5684  rabxp  5685  csbxp  5736  ssrelOLD  5744  relopabi  5783  relopabiALT  5784  cnv0  6098  dfoprab2  7420  dmoprab  7463  dfopab2  7989  brdom7disj  10476  brdom6disj  10477  opabssi  31599  cnvoprabOLD  31705  bj-dfid2ALT  35609  rnxrn  36933  dropab1  42849  dropab2  42850  csbxpgVD  43298  relopabVD  43305