Definition df-opab 5133

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 5482 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 7865. An example is given by ex-opab 28697. (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 5132	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1538	. . . . . . 7 class 𝑧
7	2	cv 1538	. . . . . . . 8 class 𝑥
8	3	cv 1538	. . . . . . . 8 class 𝑦
9	7, 8	cop 4564	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1539	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 395	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1783	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1783	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2715	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1539	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5134  opabbid  5135  opabbidv  5136  nfopabd  5138  nfopab1  5140  nfopab2  5141  cbvopab  5142  cbvopabv  5143  cbvopab1  5145  cbvopab1g  5146  cbvopab2  5147  cbvopab1s  5148  cbvopab1v  5149  cbvopab2v  5151  unopab  5152  opabidw  5431  opabid  5432  elopab  5433  ssopab2  5452  iunopab  5465  dfid2  5482  dfid3  5483  elxpi  5602  opabssxpd  5625  rabxp  5626  csbxp  5676  ssrel  5683  relopabi  5721  relopabiALT  5722  cnv0  6033  dfoprab2  7311  dmoprab  7354  dfopab2  7865  brdom7disj  10218  brdom6disj  10219  opabssi  30854  cnvoprabOLD  30957  bj-dfid2ALT  35163  rnxrn  36451  dropab1  41954  dropab2  41955  csbxpgVD  42403  relopabVD  42410