Definition df-opab 5172

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 5537 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 8033. An example is given by ex-opab 30367. (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 5171	. 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 4597	. . . . . . 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 2708	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1540	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5173  opabbid  5174  opabbidv  5175  nfopabd  5177  nfopab1  5179  nfopab2  5180  cbvopab  5181  cbvopabv  5182  cbvopab1  5183  cbvopab1g  5184  cbvopab2  5185  cbvopab1s  5186  cbvopab1v  5187  cbvopab2v  5188  unopab  5189  opabidw  5486  opabid  5487  elopabw  5488  ssopab2  5508  iunopab  5521  iunopabOLD  5522  dfid2  5537  dfid3  5538  elxpi  5662  opabssxpd  5687  rabxp  5688  csbxp  5740  ssrelOLD  5748  relopabi  5787  relopabiALT  5788  cnv0  6115  dfoprab2  7449  dmoprab  7494  dfopab2  8033  brdom7disj  10490  brdom6disj  10491  opabssi  32547  cbvopab1davw  36247  cbvopab2davw  36248  cbvopabdavw  36249  bj-dfid2ALT  37048  rnxrn  38379  dropab1  44429  dropab2  44430  csbxpgVD  44876  relopabVD  44883