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 5557 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 8047. An example is given by ex-opab 30794. (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 1568	. . . . . . 7 class 𝑧
7	2	cv 1568	. . . . . . . 8 class 𝑥
8	3	cv 1568	. . . . . . . 8 class 𝑦
9	7, 8	cop 4594	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1569	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 400	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1808	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1808	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2740	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1569	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is used 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  5507  opabid  5508  elopabw  5509  ssopab2  5530  iunopab  5543  dfid2  5557  dfid3  5558  elxpi  5682  opabssxpd  5707  rabxp  5708  csbxp  5761  relopabi  5808  relopabiALT  5809  cnv0OLD  5869  dfoprab2  7470  dmoprab  7515  dfopab2  8047  brdom7disj  10521  brdom6disj  10522  opabssi  32969  cbvopab1davw  36804  cbvopab2davw  36805  cbvopabdavw  36806  bj-dfid2ALT  37729  rnxrn  39098  dropab1  45184  dropab2  45185  csbxpgVD  45630  relopabVD  45637