Definition df-opab 5165

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 5546 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 8035. An example is given by ex-opab 30636. (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 5164	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1561	. . . . . . 7 class 𝑧
7	2	cv 1561	. . . . . . . 8 class 𝑥
8	3	cv 1561	. . . . . . . 8 class 𝑦
9	7, 8	cop 4590	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1562	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 399	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1801	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1801	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2742	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1562	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5166  opabbid  5167  opabbidv  5168  nfopabd  5170  nfopab1  5172  nfopab2  5173  cbvopab  5174  cbvopabv  5175  cbvopab1  5176  cbvopab1g  5177  cbvopab2  5178  cbvopab1s  5179  cbvopab1v  5180  cbvopab2v  5181  unopab  5182  opabidw  5496  opabid  5497  elopabw  5498  ssopab2  5519  iunopab  5532  dfid2  5546  dfid3  5547  elxpi  5671  opabssxpd  5696  rabxp  5697  csbxp  5750  relopabi  5797  relopabiALT  5798  cnv0OLD  5858  dfoprab2  7456  dmoprab  7501  dfopab2  8035  brdom7disj  10490  brdom6disj  10491  opabssi  32817  cbvopab1davw  36629  cbvopab2davw  36630  cbvopabdavw  36631  bj-dfid2ALT  37555  rnxrn  38925  dropab1  45027  dropab2  45028  csbxpgVD  45474  relopabVD  45481