ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-oprab GIF version

Definition df-oprab 5881
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 5880 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 ovmpo 6012. (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 5878 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
6 vw . . . . . . . . 9 setvar 𝑤
76cv 1352 . . . . . . . 8 class 𝑤
82cv 1352 . . . . . . . . . 10 class 𝑥
93cv 1352 . . . . . . . . . 10 class 𝑦
108, 9cop 3597 . . . . . . . . 9 class 𝑥, 𝑦
114cv 1352 . . . . . . . . 9 class 𝑧
1210, 11cop 3597 . . . . . . . 8 class ⟨⟨𝑥, 𝑦⟩, 𝑧
137, 12wceq 1353 . . . . . . 7 wff 𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧
1413, 1wa 104 . . . . . 6 wff (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1514, 4wex 1492 . . . . 5 wff 𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1615, 3wex 1492 . . . 4 wff 𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1716, 2wex 1492 . . 3 wff 𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)
1817, 6cab 2163 . 2 class {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
195, 18wceq 1353 1 wff {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
Colors of variables: wff set class
This definition is referenced by:  oprabid  5909  dfoprab2  5924  nfoprab1  5926  nfoprab2  5927  nfoprab3  5928  nfoprab  5929  oprabbid  5930  ssoprab2  5933  mpo0  5947  cbvoprab2  5950  eloprabga  5964  oprabrexex2  6133  eloprabi  6199  cnvoprab  6237  dftpos3  6265
  Copyright terms: Public domain W3C validator