Definition df-opab 5102

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 5443 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 7800. An example is given by ex-opab 28469. (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 5101	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1542	. . . . . . 7 class 𝑧
7	2	cv 1542	. . . . . . . 8 class 𝑥
8	3	cv 1542	. . . . . . . 8 class 𝑦
9	7, 8	cop 4533	. . . . . . 7 class ⟨𝑥, 𝑦⟩
10	6, 9	wceq 1543	. . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦⟩
11	10, 1	wa 399	. . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12	11, 3	wex 1787	. . . 4 wff ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13	12, 2	wex 1787	. . 3 wff ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
14	13, 5	cab 2714	. 2 class {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
15	4, 14	wceq 1543	1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}

This definition is referenced by:  opabss  5103  opabbid  5104  opabbidv  5105  nfopab  5107  nfopab1  5108  nfopab2  5109  cbvopab  5110  cbvopabv  5111  cbvopab1  5113  cbvopab1g  5114  cbvopab2  5115  cbvopab1s  5116  cbvopab2v  5118  unopab  5119  opabidw  5391  opabid  5392  elopab  5393  ssopab2  5412  iunopab  5425  dfid3  5442  elxpi  5558  opabssxpd  5581  rabxp  5582  csbxp  5632  ssrel  5639  relopabi  5677  relopabiALT  5678  cnv0  5984  dfoprab2  7247  dmoprab  7290  dfopab2  7800  brdom7disj  10110  brdom6disj  10111  opabssi  30626  cnvoprabOLD  30729  rnxrn  36210  dropab1  41679  dropab2  41680  csbxpgVD  42128  relopabVD  42135