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

Definition df-oprab 6815
Description: Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally 𝑥, 𝑦, and 𝑧 are distinct, although the definition doesn't strictly require it. See df-ov 6814 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ovmpt2 6959. (Contributed by NM, 12-Mar-1995.)
Assertion
Ref Expression
df-oprab {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
Distinct variable groups:   𝑥,𝑤   𝑦,𝑤   𝑧,𝑤   𝜑,𝑤
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Detailed syntax breakdown of Definition df-oprab
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 vz . . 3 setvar 𝑧
51, 2, 3, 4coprab 6812 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
6 vw . . . . . . . . 9 setvar 𝑤
76cv 1629 . . . . . . . 8 class 𝑤
82cv 1629 . . . . . . . . . 10 class 𝑥
93cv 1629 . . . . . . . . . 10 class 𝑦
108, 9cop 4325 . . . . . . . . 9 class 𝑥, 𝑦
114cv 1629 . . . . . . . . 9 class 𝑧
1210, 11cop 4325 . . . . . . . 8 class ⟨⟨𝑥, 𝑦⟩, 𝑧
137, 12wceq 1630 . . . . . . 7 wff 𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧
1413, 1wa 383 . . . . . 6 wff (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1514, 4wex 1851 . . . . 5 wff 𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1615, 3wex 1851 . . . 4 wff 𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1716, 2wex 1851 . . 3 wff 𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1817, 6cab 2744 . 2 class {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
195, 18wceq 1630 1 wff {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  oprabid  6838  dfoprab2  6864  nfoprab1  6867  nfoprab2  6868  nfoprab3  6869  nfoprab  6870  oprabbid  6871  ssoprab2  6874  mpt20  6888  cbvoprab2  6891  eloprabga  6910  oprabrexex2  7321  eloprabi  7398  dftpos3  7537  meet0  17336  join0  17337  cnvoprabOLD  29805  mppspstlem  31773  mppsval  31774  colinearex  32471  csboprabg  33485
  Copyright terms: Public domain W3C validator