Definition df-opab 5167

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 5547 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 8063. An example is given by ex-opab 31033. (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 5166	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1568	. . . . . . 7 class 𝑧
7	2	cv 1568	. . . . . . . 8 class 𝑥
8	3	cv 1568	. . . . . . . 8 class 𝑦
9	7, 8	cop 4589	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1569	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 401	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1811	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1811	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2738	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1569	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is used by:  opabss  5168  opabbid  5169  opabbidv  5170  nfopabd  5172  nfopab1  5174  nfopab2  5175  cbvopab  5176  cbvopabv  5177  cbvopab1  5178  cbvopab1g  5179  cbvopab2  5180  cbvopab1s  5181  cbvopab1v  5182  cbvopab2v  5183  unopab  5184  opabidw  5497  opabid  5498  elopabw  5499  ssopab2  5520  iunopab  5533  dfid2  5547  dfid3  5548  elxpi  5672  opabssxpd  5697  rabxp  5698  csbxp  5751  relopabi  5799  relopabiALT  5800  cnv0OLD  5861  dfoprab2  7478  dmoprab  7523  dfopab2  8063  brdom7disj  10610  brdom6disj  10611  opabssi  33249  cbvopab1davw  37095  cbvopab2davw  37096  cbvopabdavw  37097  bj-dfid2ALT  38022  rnxrn  39396  dropab1  45472  dropab2  45473  csbxpgVD  45918  relopabVD  45925