Definition df-opab 5173

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 5558 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 8048. An example is given by ex-opab 30749. (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 5172	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1567	. . . . . . 7 class 𝑧
7	2	cv 1567	. . . . . . . 8 class 𝑥
8	3	cv 1567	. . . . . . . 8 class 𝑦
9	7, 8	cop 4594	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1568	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 400	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1807	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1807	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2739	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1568	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5174  opabbid  5175  opabbidv  5176  nfopabd  5178  nfopab1  5180  nfopab2  5181  cbvopab  5182  cbvopabv  5183  cbvopab1  5184  cbvopab1g  5185  cbvopab2  5186  cbvopab1s  5187  cbvopab1v  5188  cbvopab2v  5189  unopab  5190  opabidw  5508  opabid  5509  elopabw  5510  ssopab2  5531  iunopab  5544  dfid2  5558  dfid3  5559  elxpi  5683  opabssxpd  5708  rabxp  5709  csbxp  5762  relopabi  5809  relopabiALT  5810  cnv0OLD  5870  dfoprab2  7468  dmoprab  7513  dfopab2  8048  brdom7disj  10514  brdom6disj  10515  opabssi  32924  cbvopab1davw  36720  cbvopab2davw  36721  cbvopabdavw  36722  bj-dfid2ALT  37645  rnxrn  39016  dropab1  45104  dropab2  45105  csbxpgVD  45550  relopabVD  45557