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 8034. An example is given by ex-opab 30368. (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 1539	. . . . . . 7 class 𝑧
7	2	cv 1539	. . . . . . . 8 class 𝑥
8	3	cv 1539	. . . . . . . 8 class 𝑦
9	7, 8	cop 4598	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1540	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 395	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1779	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1779	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2708	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1540	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5174  opabbid  5175  opabbidv  5176  nfopabd  5178  nfopab1  5180  nfopab2  5181  cbvopab  5182  cbvopabv  5183  cbvopab1  5184  cbvopab1g  5185  cbvopab2  5186  cbvopab1s  5187  cbvopab1v  5188  cbvopab2v  5189  unopab  5190  opabidw  5487  opabid  5488  elopabw  5489  ssopab2  5509  iunopab  5522  iunopabOLD  5523  dfid2  5538  dfid3  5539  elxpi  5663  opabssxpd  5688  rabxp  5689  csbxp  5741  ssrelOLD  5749  relopabi  5788  relopabiALT  5789  cnv0  6116  dfoprab2  7450  dmoprab  7495  dfopab2  8034  brdom7disj  10491  brdom6disj  10492  opabssi  32548  cbvopab1davw  36259  cbvopab2davw  36260  cbvopabdavw  36261  bj-dfid2ALT  37060  rnxrn  38391  dropab1  44443  dropab2  44444  csbxpgVD  44890  relopabVD  44897