Definition df-opab 5229

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 5595 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 8093. An example is given by ex-opab 30464. (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 5228	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1536	. . . . . . 7 class 𝑧
7	2	cv 1536	. . . . . . . 8 class 𝑥
8	3	cv 1536	. . . . . . . 8 class 𝑦
9	7, 8	cop 4654	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1537	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 395	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1777	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1777	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2717	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1537	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5230  opabbid  5231  opabbidv  5232  nfopabd  5234  nfopab1  5236  nfopab2  5237  cbvopab  5238  cbvopabv  5239  cbvopab1  5241  cbvopab1g  5242  cbvopab2  5243  cbvopab1s  5244  cbvopab1v  5245  cbvopab2v  5247  unopab  5248  opabidw  5543  opabid  5544  elopabw  5545  ssopab2  5565  iunopab  5578  iunopabOLD  5579  dfid2  5595  dfid3  5596  elxpi  5722  opabssxpd  5747  rabxp  5748  csbxp  5799  ssrelOLD  5807  relopabi  5846  relopabiALT  5847  cnv0  6172  dfoprab2  7508  dmoprab  7552  dfopab2  8093  brdom7disj  10600  brdom6disj  10601  opabssi  32635  cnvoprabOLD  32734  cbvopab1davw  36230  cbvopab2davw  36231  cbvopabdavw  36232  bj-dfid2ALT  37031  rnxrn  38354  dropab1  44416  dropab2  44417  csbxpgVD  44865  relopabVD  44872