Definition df-opab 5129

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 does not require it (see dfid2 5463 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also called "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 7750. An example is given by ex-opab 28211. (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 5128	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1536	. . . . . . 7 class 𝑧
7	2	cv 1536	. . . . . . . 8 class 𝑥
8	3	cv 1536	. . . . . . . 8 class 𝑦
9	7, 8	cop 4573	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1537	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 398	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1780	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1780	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2799	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1537	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5130  opabbid  5131  nfopab  5134  nfopab1  5135  nfopab2  5136  cbvopab  5137  cbvopab1  5139  cbvopab1g  5140  cbvopab2  5141  cbvopab1s  5142  cbvopab2v  5144  unopab  5145  opabidw  5412  opabid  5413  elopab  5414  ssopab2  5433  iunopab  5446  dfid3  5462  elxpi  5577  rabxp  5600  csbxp  5650  ssrel  5657  relopabi  5694  relopabiALT  5695  opabssxpd  5789  cnv0  5999  dfoprab2  7212  dmoprab  7255  dfopab2  7750  brdom7disj  9953  brdom6disj  9954  opabssi  30364  cnvoprabOLD  30456  rnxrn  35661  dropab1  40828  dropab2  40829  csbxpgVD  41277  relopabVD  41284