Definition df-opab 5149

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 5525 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 8002. An example is given by ex-opab 30499. (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 5148	. 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 4574	. . . . . . 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  5150  opabbid  5151  opabbidv  5152  nfopabd  5154  nfopab1  5156  nfopab2  5157  cbvopab  5158  cbvopabv  5159  cbvopab1  5160  cbvopab1g  5161  cbvopab2  5162  cbvopab1s  5163  cbvopab1v  5164  cbvopab2v  5165  unopab  5166  opabidw  5476  opabid  5477  elopabw  5478  ssopab2  5498  iunopab  5511  dfid2  5525  dfid3  5526  elxpi  5650  opabssxpd  5675  rabxp  5676  csbxp  5729  relopabi  5775  relopabiALT  5776  cnv0OLD  6102  dfoprab2  7422  dmoprab  7467  dfopab2  8002  brdom7disj  10450  brdom6disj  10451  opabssi  32683  cbvopab1davw  36443  cbvopab2davw  36444  cbvopabdavw  36445  bj-dfid2ALT  37369  rnxrn  38739  dropab1  44870  dropab2  44871  csbxpgVD  45317  relopabVD  45324