Definition df-opab 4992

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 doesn't strictly require it (see dfid2 5315 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 7558. For example, 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 27989). (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 4991	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1506	. . . . . . 7 class 𝑧
7	2	cv 1506	. . . . . . . 8 class 𝑥
8	3	cv 1506	. . . . . . . 8 class 𝑦
9	7, 8	cop 4447	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1507	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 387	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1742	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1742	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2759	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1507	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  4993  opabbid  4994  nfopab  4997  nfopab1  4998  nfopab2  4999  cbvopab  5000  cbvopab1  5002  cbvopab2  5003  cbvopab1s  5004  cbvopab2v  5006  unopab  5007  opabid  5268  elopab  5269  ssopab2  5287  iunopab  5298  dfid3  5313  elxpi  5429  rabxp  5452  csbxp  5500  ssrel  5507  relopabi  5544  relopabiALT  5545  opabssxpd  5636  cnv0  5839  dfoprab2  7031  dmoprab  7071  dfopab2  7558  brdom7disj  9751  brdom6disj  9752  opabssi  30128  cnvoprabOLD  30208  rnxrn  35088  dropab1  40195  dropab2  40196  csbxpgVD  40644  relopabVD  40651