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 7435
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 7434 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 an operation given by a class abstraction is given by ovmpo 7593. (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 7432 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
6 vw . . . . . . . . 9 setvar 𝑤
76cv 1539 . . . . . . . 8 class 𝑤
82cv 1539 . . . . . . . . . 10 class 𝑥
93cv 1539 . . . . . . . . . 10 class 𝑦
108, 9cop 4632 . . . . . . . . 9 class 𝑥, 𝑦
114cv 1539 . . . . . . . . 9 class 𝑧
1210, 11cop 4632 . . . . . . . 8 class ⟨⟨𝑥, 𝑦⟩, 𝑧
137, 12wceq 1540 . . . . . . 7 wff 𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧
1413, 1wa 395 . . . . . 6 wff (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1514, 4wex 1779 . . . . 5 wff 𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1615, 3wex 1779 . . . 4 wff 𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1716, 2wex 1779 . . 3 wff 𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1817, 6cab 2714 . 2 class {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
195, 18wceq 1540 1 wff {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  oprabidw  7462  oprabid  7463  dfoprab2  7491  nfoprab1  7494  nfoprab2  7495  nfoprab3  7496  nfoprab  7497  oprabbid  7498  oprabbidv  7499  ssoprab2  7501  0mpo0  7516  mpo0  7518  cbvoprab2  7521  cbvoprab12v  7523  cbvoprab3v  7525  eloprabga  7542  oprabrexex2  8003  eloprabi  8088  dftpos3  8269  join0  18450  meet0  18451  mppspstlem  35576  mppsval  35577  colinearex  36061  cbvoprab1vw  36238  cbvoprab2vw  36239  cbvoprab123vw  36240  cbvoprab23vw  36241  cbvoprab13vw  36242  cbvoprab1davw  36272  cbvoprab2davw  36273  cbvoprab3davw  36274  cbvoprab123davw  36275  cbvoprab12davw  36276  cbvoprab23davw  36277  cbvoprab13davw  36278  csboprabg  37331
  Copyright terms: Public domain W3C validator