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 5556 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 8052. An example is given by ex-opab 30898. (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 1569	. . . . . . 7 class 𝑧
7	2	cv 1569	. . . . . . . 8 class 𝑥
8	3	cv 1569	. . . . . . . 8 class 𝑦
9	7, 8	cop 4593	. . . . . . 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 2740	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1570	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is used 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  5506  opabid  5507  elopabw  5508  ssopab2  5529  iunopab  5542  dfid2  5556  dfid3  5557  elxpi  5681  opabssxpd  5706  rabxp  5707  csbxp  5760  relopabi  5807  relopabiALT  5808  cnv0OLD  5868  dfoprab2  7474  dmoprab  7519  dfopab2  8052  brdom7disj  10537  brdom6disj  10538  opabssi  33073  cbvopab1davw  36871  cbvopab2davw  36872  cbvopabdavw  36873  bj-dfid2ALT  37796  rnxrn  39156  dropab1  45257  dropab2  45258  csbxpgVD  45703  relopabVD  45710