Definition df-opab 4907

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 5222 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 7450. For example, 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 27616). (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 4906	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1636	. . . . . . 7 class 𝑧
7	2	cv 1636	. . . . . . . 8 class 𝑥
8	3	cv 1636	. . . . . . . 8 class 𝑦
9	7, 8	cop 4376	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1637	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 384	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1859	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1859	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2792	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1637	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  4908  opabbid  4909  nfopab  4912  nfopab1  4913  nfopab2  4914  cbvopab  4915  cbvopab1  4917  cbvopab2  4918  cbvopab1s  4919  cbvopab2v  4921  unopab  4922  opabid  5177  elopab  5178  ssopab2  5196  iunopab  5207  dfid3  5220  elxpi  5332  rabxp  5354  csbxp  5402  ssrel  5409  relopabi  5447  relopabiALT  5448  opabssxpd  5539  cnv0  5746  dfoprab2  6927  dmoprab  6967  dfopab2  7450  brdom7disj  9634  brdom6disj  9635  opabssi  29746  cnvoprabOLD  29821  cnfinltrel  33552  rnxrn  34464  dropab1  39143  dropab2  39144  csbxpgOLD  39542  csbxpgVD  39618  relopabVD  39625