Definition df-opab 5210

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 5575 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 8040. An example is given by ex-opab 29952. (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 5209	. 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 4633	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1539	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 394	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1779	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1779	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2707	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1539	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5211  opabbid  5212  opabbidv  5213  nfopabd  5215  nfopab1  5217  nfopab2  5218  cbvopab  5219  cbvopabv  5220  cbvopab1  5222  cbvopab1g  5223  cbvopab2  5224  cbvopab1s  5225  cbvopab1v  5226  cbvopab2v  5228  unopab  5229  opabidw  5523  opabid  5524  elopabw  5525  ssopab2  5545  iunopab  5558  iunopabOLD  5559  dfid2  5575  dfid3  5576  elxpi  5697  opabssxpd  5722  rabxp  5723  csbxp  5774  ssrelOLD  5782  relopabi  5821  relopabiALT  5822  cnv0  6139  dfoprab2  7469  dmoprab  7512  dfopab2  8040  brdom7disj  10528  brdom6disj  10529  opabssi  32109  cnvoprabOLD  32212  bj-dfid2ALT  36249  rnxrn  37571  dropab1  43508  dropab2  43509  csbxpgVD  43957  relopabVD  43964