Definition df-opab 5159

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 5524 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 7964. An example is given by ex-opab 29083. (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 5158	. 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 4583	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1541	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 397	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1781	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1781	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2714	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1541	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5160  opabbid  5161  opabbidv  5162  nfopabd  5164  nfopab1  5166  nfopab2  5167  cbvopab  5168  cbvopabv  5169  cbvopab1  5171  cbvopab1g  5172  cbvopab2  5173  cbvopab1s  5174  cbvopab1v  5175  cbvopab2v  5177  unopab  5178  opabidw  5472  opabid  5473  elopabw  5474  ssopab2  5494  iunopab  5507  iunopabOLD  5508  dfid2  5524  dfid3  5525  elxpi  5646  opabssxpd  5669  rabxp  5670  csbxp  5721  ssrelOLD  5729  relopabi  5768  relopabiALT  5769  cnv0  6083  dfoprab2  7399  dmoprab  7442  dfopab2  7964  brdom7disj  10392  brdom6disj  10393  opabssi  31238  cnvoprabOLD  31340  bj-dfid2ALT  35390  rnxrn  36716  dropab1  42438  dropab2  42439  csbxpgVD  42887  relopabVD  42894