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

Definition df-oprab 5431
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 x, y, and z are distinct, although the definition doesn't strictly require it. See df-ov 5430 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 5550. (Contributed by NM, 12-Mar-1995.)
Assertion
Ref Expression
df-oprab {⟨⟨x, y⟩, z⟩ ∣ φ} = {wxyz(w = ⟨⟨x, y⟩, z φ)}
Distinct variable groups:   x,w   y,w   z,w   φ,w
Allowed substitution hints:   φ(x,y,z)

Detailed syntax breakdown of Definition df-oprab
StepHypRef Expression
1 wph . . 3 wff φ
2 vx . . 3 setvar x
3 vy . . 3 setvar y
4 vz . . 3 setvar z
51, 2, 3, 4coprab 5428 . 2 class {⟨⟨x, y⟩, z⟩ ∣ φ}
6 vw . . . . . . . . 9 setvar w
76cv 1225 . . . . . . . 8 class w
82cv 1225 . . . . . . . . . 10 class x
93cv 1225 . . . . . . . . . 10 class y
108, 9cop 3345 . . . . . . . . 9 class x, y
114cv 1225 . . . . . . . . 9 class z
1210, 11cop 3345 . . . . . . . 8 class ⟨⟨x, y⟩, z
137, 12wceq 1226 . . . . . . 7 wff w = ⟨⟨x, y⟩, z
1413, 1wa 97 . . . . . 6 wff (w = ⟨⟨x, y⟩, z φ)
1514, 4wex 1357 . . . . 5 wff z(w = ⟨⟨x, y⟩, z φ)
1615, 3wex 1357 . . . 4 wff yz(w = ⟨⟨x, y⟩, z φ)
1716, 2wex 1357 . . 3 wff xyz(w = ⟨⟨x, y⟩, z φ)
1817, 6cab 2002 . 2 class {wxyz(w = ⟨⟨x, y⟩, z φ)}
195, 18wceq 1226 1 wff {⟨⟨x, y⟩, z⟩ ∣ φ} = {wxyz(w = ⟨⟨x, y⟩, z φ)}
Colors of variables: wff set class
This definition is referenced by:  oprabid  5452  dfoprab2  5466  nfoprab1  5468  nfoprab2  5469  nfoprab3  5470  nfoprab  5471  oprabbid  5472  ssoprab2  5475  mpt20  5488  cbvoprab2  5491  eloprabga  5505  oprabrexex2  5671  eloprabi  5736  dftpos3  5790
  Copyright terms: Public domain W3C validator