Definition df-opab 5138

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 5492 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 7901. An example is given by ex-opab 28805. (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 5137	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1538	. . . . . . 7 class 𝑧
7	2	cv 1538	. . . . . . . 8 class 𝑥
8	3	cv 1538	. . . . . . . 8 class 𝑦
9	7, 8	cop 4568	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1539	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 396	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1782	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1782	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2716	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1539	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5139  opabbid  5140  opabbidv  5141  nfopabd  5143  nfopab1  5145  nfopab2  5146  cbvopab  5147  cbvopabv  5148  cbvopab1  5150  cbvopab1g  5151  cbvopab2  5152  cbvopab1s  5153  cbvopab1v  5154  cbvopab2v  5156  unopab  5157  opabidw  5438  opabid  5439  elopabw  5440  ssopab2  5460  iunopab  5473  iunopabOLD  5474  dfid2  5492  dfid3  5493  elxpi  5612  opabssxpd  5635  rabxp  5636  csbxp  5687  ssrelOLD  5695  relopabi  5734  relopabiALT  5735  cnv0  6049  dfoprab2  7342  dmoprab  7385  dfopab2  7901  brdom7disj  10296  brdom6disj  10297  opabssi  30962  cnvoprabOLD  31064  bj-dfid2ALT  35245  rnxrn  36531  dropab1  42072  dropab2  42073  csbxpgVD  42521  relopabVD  42528