Definition df-opab 4644

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 4956 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 7113. For example, 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 26681). (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 4642	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1474	. . . . . . 7 class 𝑧
7	2	cv 1474	. . . . . . . 8 class 𝑥
8	3	cv 1474	. . . . . . . 8 class 𝑦
9	7, 8	cop 4131	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1475	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 383	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1695	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1695	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2596	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1475	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  4646  opabbid  4647  nfopab  4650  nfopab1  4651  nfopab2  4652  cbvopab  4653  cbvopab1  4655  cbvopab2  4656  cbvopab1s  4657  cbvopab2v  4659  unopab  4660  opabid  4907  elopab  4908  ssopab2  4926  iunopab  4936  dfid3  4954  elxpi  5054  rabxp  5078  csbxp  5123  ssrel  5130  relopabi  5167  relopabiALT  5168  cnv0  5454  dfoprab2  6599  dmoprab  6639  opabex2  6997  dfopab2  7113  brdom7disj  9234  brdom6disj  9235  cnvoprab  28886  dropab1  37672  dropab2  37673  csbxpgOLD  38075  csbxpgVD  38152  relopabVD  38159