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 5584 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 8075. An example is given by ex-opab 30460. (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 1535	. . . . . . 7 class 𝑧
7	2	cv 1535	. . . . . . . 8 class 𝑥
8	3	cv 1535	. . . . . . . 8 class 𝑦
9	7, 8	cop 4636	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1536	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 395	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1775	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1775	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2711	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1536	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  5533  opabid  5534  elopabw  5535  ssopab2  5555  iunopab  5568  iunopabOLD  5569  dfid2  5584  dfid3  5585  elxpi  5710  opabssxpd  5735  rabxp  5736  csbxp  5787  ssrelOLD  5795  relopabi  5834  relopabiALT  5835  cnv0  6162  dfoprab2  7490  dmoprab  7534  dfopab2  8075  brdom7disj  10568  brdom6disj  10569  opabssi  32632  cnvoprabOLD  32737  cbvopab1davw  36246  cbvopab2davw  36247  cbvopabdavw  36248  bj-dfid2ALT  37047  rnxrn  38379  dropab1  44442  dropab2  44443  csbxpgVD  44891  relopabVD  44898