Definition df-opab 5171

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 5552 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 8085. An example is given by ex-opab 31060. (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 5170	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1569	. . . . . . 7 class 𝑧
7	2	cv 1569	. . . . . . . 8 class 𝑥
8	3	cv 1569	. . . . . . . 8 class 𝑦
9	7, 8	cop 4838	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1570	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 401	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1812	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1812	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2741	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1570	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is used by:  opabss  5172  opabbid  5173  opabbidv  5174  nfopabd  5176  nfopab1  5178  nfopab2  5179  cbvopab  5180  cbvopabv  5181  cbvopab1  5182  cbvopab1g  5183  cbvopab2  5184  cbvopab1s  5185  cbvopab1v  5186  cbvopab2v  5187  unopab  5188  opabidw  5502  opabid  5503  elopabw  5504  ssopab2  5525  iunopab  5538  dfid2  5552  dfid3  5553  elxpi  5677  opabssxpd  5702  rabxp  5703  csbxp  5757  relopabi  5805  relopabiALT  5806  cnv0OLD  5868  dfoprab2  7498  dmoprab  7543  dfopab2  8085  brdom7disj  10634  brdom6disj  10635  opabssi  33276  cbvopab1davw  37230  cbvopab2davw  37231  cbvopabdavw  37232  bj-dfid2ALT  38170  rnxrn  39544  dropab1  45619  dropab2  45620  csbxpgVD  46065  relopabVD  46072