Definition df-opab 5211

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 5576 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 29940. (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 5210	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1540	. . . . . . 7 class 𝑧
7	2	cv 1540	. . . . . . . 8 class 𝑥
8	3	cv 1540	. . . . . . . 8 class 𝑦
9	7, 8	cop 4634	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1541	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 396	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1781	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1781	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2709	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1541	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5212  opabbid  5213  opabbidv  5214  nfopabd  5216  nfopab1  5218  nfopab2  5219  cbvopab  5220  cbvopabv  5221  cbvopab1  5223  cbvopab1g  5224  cbvopab2  5225  cbvopab1s  5226  cbvopab1v  5227  cbvopab2v  5229  unopab  5230  opabidw  5524  opabid  5525  elopabw  5526  ssopab2  5546  iunopab  5559  iunopabOLD  5560  dfid2  5576  dfid3  5577  elxpi  5698  opabssxpd  5723  rabxp  5724  csbxp  5775  ssrelOLD  5783  relopabi  5822  relopabiALT  5823  cnv0  6140  dfoprab2  7469  dmoprab  7512  dfopab2  8040  brdom7disj  10528  brdom6disj  10529  opabssi  32097  cnvoprabOLD  32200  bj-dfid2ALT  36249  rnxrn  37571  dropab1  43508  dropab2  43509  csbxpgVD  43957  relopabVD  43964