Definition df-opab 5182

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 5550 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 8049. An example is given by ex-opab 30359. (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 5181	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1539	. . . . . . 7 class 𝑧
7	2	cv 1539	. . . . . . . 8 class 𝑥
8	3	cv 1539	. . . . . . . 8 class 𝑦
9	7, 8	cop 4607	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1540	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 395	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1779	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1779	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2713	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1540	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5183  opabbid  5184  opabbidv  5185  nfopabd  5187  nfopab1  5189  nfopab2  5190  cbvopab  5191  cbvopabv  5192  cbvopab1  5193  cbvopab1g  5194  cbvopab2  5195  cbvopab1s  5196  cbvopab1v  5197  cbvopab2v  5199  unopab  5200  opabidw  5499  opabid  5500  elopabw  5501  ssopab2  5521  iunopab  5534  iunopabOLD  5535  dfid2  5550  dfid3  5551  elxpi  5676  opabssxpd  5701  rabxp  5702  csbxp  5754  ssrelOLD  5762  relopabi  5801  relopabiALT  5802  cnv0  6129  dfoprab2  7463  dmoprab  7508  dfopab2  8049  brdom7disj  10543  brdom6disj  10544  opabssi  32539  cbvopab1davw  36228  cbvopab2davw  36229  cbvopabdavw  36230  bj-dfid2ALT  37029  rnxrn  38362  dropab1  44419  dropab2  44420  csbxpgVD  44866  relopabVD  44873