Definition df-opab 5208

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 5574 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 8058. An example is given by ex-opab 30362. (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 5207	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1533	. . . . . . 7 class 𝑧
7	2	cv 1533	. . . . . . . 8 class 𝑥
8	3	cv 1533	. . . . . . . 8 class 𝑦
9	7, 8	cop 4629	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1534	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 394	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1774	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1774	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2703	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1534	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5209  opabbid  5210  opabbidv  5211  nfopabd  5213  nfopab1  5215  nfopab2  5216  cbvopab  5217  cbvopabv  5218  cbvopab1  5220  cbvopab1g  5221  cbvopab2  5222  cbvopab1s  5223  cbvopab1v  5224  cbvopab2v  5226  unopab  5227  opabidw  5522  opabid  5523  elopabw  5524  ssopab2  5544  iunopab  5557  iunopabOLD  5558  dfid2  5574  dfid3  5575  elxpi  5696  opabssxpd  5721  rabxp  5722  csbxp  5773  ssrelOLD  5781  relopabi  5820  relopabiALT  5821  cnv0  6144  dfoprab2  7475  dmoprab  7519  dfopab2  8058  brdom7disj  10565  brdom6disj  10566  opabssi  32533  cnvoprabOLD  32634  bj-dfid2ALT  36785  rnxrn  38109  dropab1  44158  dropab2  44159  csbxpgVD  44607  relopabVD  44614