Definition df-opab 5137

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 5517 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 7996. An example is given by ex-opab 30522. (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 5136	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1547	. . . . . . 7 class 𝑧
7	2	cv 1547	. . . . . . . 8 class 𝑥
8	3	cv 1547	. . . . . . . 8 class 𝑦
9	7, 8	cop 4563	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1548	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 397	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1787	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1787	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2719	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1548	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5138  opabbid  5139  opabbidv  5140  nfopabd  5142  nfopab1  5144  nfopab2  5145  cbvopab  5146  cbvopabv  5147  cbvopab1  5148  cbvopab1g  5149  cbvopab2  5150  cbvopab1s  5151  cbvopab1v  5152  cbvopab2v  5153  unopab  5154  opabidw  5468  opabid  5469  elopabw  5470  ssopab2  5490  iunopab  5503  dfid2  5517  dfid3  5518  elxpi  5642  opabssxpd  5667  rabxp  5668  csbxp  5721  relopabi  5767  relopabiALT  5768  cnv0OLD  5828  dfoprab2  7417  dmoprab  7462  dfopab2  7996  brdom7disj  10449  brdom6disj  10450  opabssi  32707  cbvopab1davw  36505  cbvopab2davw  36506  cbvopabdavw  36507  bj-dfid2ALT  37431  rnxrn  38801  dropab1  44903  dropab2  44904  csbxpgVD  45350  relopabVD  45357