Definition df-opab 4746

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 5056 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 7266. For example, 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 27419). (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 4745	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1522	. . . . . . 7 class 𝑧
7	2	cv 1522	. . . . . . . 8 class 𝑥
8	3	cv 1522	. . . . . . . 8 class 𝑦
9	7, 8	cop 4216	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1523	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 383	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1744	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1744	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2637	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1523	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  4747  opabbid  4748  nfopab  4751  nfopab1  4752  nfopab2  4753  cbvopab  4754  cbvopab1  4756  cbvopab2  4757  cbvopab1s  4758  cbvopab2v  4760  unopab  4761  opabid  5011  elopab  5012  ssopab2  5030  iunopab  5041  dfid3  5054  elxpi  5164  rabxp  5188  csbxp  5234  ssrel  5241  relopabi  5278  relopabiALT  5279  opabssxpd  5370  cnv0  5570  dfoprab2  6743  dmoprab  6783  dfopab2  7266  brdom7disj  9391  brdom6disj  9392  opabssi  29551  cnvoprabOLD  29626  rnxrn  34296  dropab1  38968  dropab2  38969  csbxpgOLD  39368  csbxpgVD  39444  relopabVD  39451