NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-opab GIF version

Definition df-opab 4623
Description: Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually x and y are distinct, although the definition doesn't strictly require it (see dfid2 4769 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
df-opab {x, y φ} = {z xy(z = x, y φ)}
Distinct variable groups:   x,z   y,z   φ,z
Allowed substitution hints:   φ(x,y)

Detailed syntax breakdown of Definition df-opab
StepHypRef Expression
1 wph . . 3 wff φ
2 vx . . 3 setvar x
3 vy . . 3 setvar y
41, 2, 3copab 4622 . 2 class {x, y φ}
5 vz . . . . . . . 8 setvar z
65cv 1641 . . . . . . 7 class z
72cv 1641 . . . . . . . 8 class x
83cv 1641 . . . . . . . 8 class y
97, 8cop 4561 . . . . . . 7 class x, y
106, 9wceq 1642 . . . . . 6 wff z = x, y
1110, 1wa 358 . . . . 5 wff (z = x, y φ)
1211, 3wex 1541 . . . 4 wff y(z = x, y φ)
1312, 2wex 1541 . . 3 wff xy(z = x, y φ)
1413, 5cab 2339 . 2 class {z xy(z = x, y φ)}
154, 14wceq 1642 1 wff {x, y φ} = {z xy(z = x, y φ)}
Colors of variables: wff setvar class
This definition is referenced by:  opabbid  4624  nfopab  4627  nfopab1  4628  nfopab2  4629  cbvopab  4630  cbvopab1  4632  cbvopab2  4633  cbvopab1s  4634  cbvopab2v  4636  unopab  4638  opabid  4695  elopab  4696  ssopab2  4712  dfid3  4768  elxpi  4800  csbxpg  4813  rabxp  4814  iunfopab  5204  dfoprab2  5558  dmoprab  5574
  Copyright terms: Public domain W3C validator