MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-opab Structured version   Visualization version   GIF version

Definition df-opab 5206
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 5580 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 8077. An example is given by ex-opab 30451. (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
df-opab {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Distinct variable groups:   𝑥,𝑧   𝑦,𝑧   𝜑,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦)

Detailed syntax breakdown of Definition df-opab
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
41, 2, 3copab 5205 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1539 . . . . . . 7 class 𝑧
72cv 1539 . . . . . . . 8 class 𝑥
83cv 1539 . . . . . . . 8 class 𝑦
97, 8cop 4632 . . . . . . 7 class 𝑥, 𝑦
106, 9wceq 1540 . . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦
1110, 1wa 395 . . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211, 3wex 1779 . . . 4 wff 𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312, 2wex 1779 . . 3 wff 𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1413, 5cab 2714 . 2 class {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
154, 14wceq 1540 1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  opabss  5207  opabbid  5208  opabbidv  5209  nfopabd  5211  nfopab1  5213  nfopab2  5214  cbvopab  5215  cbvopabv  5216  cbvopab1  5217  cbvopab1g  5218  cbvopab2  5219  cbvopab1s  5220  cbvopab1v  5221  cbvopab2v  5223  unopab  5224  opabidw  5529  opabid  5530  elopabw  5531  ssopab2  5551  iunopab  5564  iunopabOLD  5565  dfid2  5580  dfid3  5581  elxpi  5707  opabssxpd  5732  rabxp  5733  csbxp  5785  ssrelOLD  5793  relopabi  5832  relopabiALT  5833  cnv0  6160  dfoprab2  7491  dmoprab  7536  dfopab2  8077  brdom7disj  10571  brdom6disj  10572  opabssi  32625  cbvopab1davw  36265  cbvopab2davw  36266  cbvopabdavw  36267  bj-dfid2ALT  37066  rnxrn  38399  dropab1  44466  dropab2  44467  csbxpgVD  44914  relopabVD  44921
  Copyright terms: Public domain W3C validator