Definition df-opab 4857

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 5169 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 7381. For example, 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 27592). (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 4856	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1623	. . . . . . 7 class 𝑧
7	2	cv 1623	. . . . . . . 8 class 𝑥
8	3	cv 1623	. . . . . . . 8 class 𝑦
9	7, 8	cop 4319	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1624	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 383	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1845	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1845	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2738	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1624	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  4858  opabbid  4859  nfopab  4862  nfopab1  4863  nfopab2  4864  cbvopab  4865  cbvopab1  4867  cbvopab2  4868  cbvopab1s  4869  cbvopab2v  4871  unopab  4872  opabid  5124  elopab  5125  ssopab2  5143  iunopab  5154  dfid3  5167  elxpi  5279  rabxp  5303  csbxp  5349  ssrel  5356  relopabi  5393  relopabiALT  5394  opabssxpd  5485  cnv0  5685  dfoprab2  6858  dmoprab  6898  dfopab2  7381  brdom7disj  9537  brdom6disj  9538  opabssi  29724  cnvoprabOLD  29799  cnfinltrel  33544  rnxrn  34471  dropab1  39145  dropab2  39146  csbxpgOLD  39545  csbxpgVD  39621  relopabVD  39628