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

Definition df-oprab 7146
 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 7145 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 7297. (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 7143 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
6 vw . . . . . . . . 9 setvar 𝑤
76cv 1537 . . . . . . . 8 class 𝑤
82cv 1537 . . . . . . . . . 10 class 𝑥
93cv 1537 . . . . . . . . . 10 class 𝑦
108, 9cop 4533 . . . . . . . . 9 class 𝑥, 𝑦
114cv 1537 . . . . . . . . 9 class 𝑧
1210, 11cop 4533 . . . . . . . 8 class ⟨⟨𝑥, 𝑦⟩, 𝑧
137, 12wceq 1538 . . . . . . 7 wff 𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧
1413, 1wa 399 . . . . . 6 wff (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1514, 4wex 1781 . . . . 5 wff 𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1615, 3wex 1781 . . . 4 wff 𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1716, 2wex 1781 . . 3 wff 𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1817, 6cab 2776 . 2 class {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
195, 18wceq 1538 1 wff {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
 Colors of variables: wff setvar class This definition is referenced by:  oprabidw  7173  oprabid  7174  dfoprab2  7198  nfoprab1  7201  nfoprab2  7202  nfoprab3  7203  nfoprab  7204  oprabbid  7205  ssoprab2  7208  0mpo0  7223  mpo0  7225  cbvoprab2  7228  eloprabga  7247  oprabrexex2  7671  eloprabi  7753  dftpos3  7908  meet0  17756  join0  17757  cnvoprabOLD  30523  mppspstlem  32994  mppsval  32995  colinearex  33697  csboprabg  34814
 Copyright terms: Public domain W3C validator