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 6874
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 6873 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 7022. (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 6871 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
6 vw . . . . . . . . 9 setvar 𝑤
76cv 1636 . . . . . . . 8 class 𝑤
82cv 1636 . . . . . . . . . 10 class 𝑥
93cv 1636 . . . . . . . . . 10 class 𝑦
108, 9cop 4376 . . . . . . . . 9 class 𝑥, 𝑦
114cv 1636 . . . . . . . . 9 class 𝑧
1210, 11cop 4376 . . . . . . . 8 class ⟨⟨𝑥, 𝑦⟩, 𝑧
137, 12wceq 1637 . . . . . . 7 wff 𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧
1413, 1wa 384 . . . . . 6 wff (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1514, 4wex 1859 . . . . 5 wff 𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1615, 3wex 1859 . . . 4 wff 𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1716, 2wex 1859 . . 3 wff 𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1817, 6cab 2792 . 2 class {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
195, 18wceq 1637 1 wff {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  oprabid  6901  dfoprab2  6927  nfoprab1  6930  nfoprab2  6931  nfoprab3  6932  nfoprab  6933  oprabbid  6934  ssoprab2  6937  mpt20  6951  cbvoprab2  6954  eloprabga  6973  oprabrexex2  7384  eloprabi  7461  dftpos3  7601  meet0  17338  join0  17339  cnvoprabOLD  29821  mppspstlem  31786  mppsval  31787  colinearex  32483  csboprabg  33488
  Copyright terms: Public domain W3C validator