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

Definition df-opab 3960
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. The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
df-opab  |-  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
Distinct variable groups:    x, z    y,
z    ph, z
Allowed substitution hints:    ph( x, y)

Detailed syntax breakdown of Definition df-opab
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
41, 2, 3copab 3958 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  setvar  z
65cv 1315 . . . . . . 7  class  z
72cv 1315 . . . . . . . 8  class  x
83cv 1315 . . . . . . . 8  class  y
97, 8cop 3500 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1316 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 103 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1453 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1453 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2103 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1316 1  wff  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
Colors of variables: wff set class
This definition is referenced by:  opabss  3962  opabbid  3963  nfopab  3966  nfopab1  3967  nfopab2  3968  cbvopab  3969  cbvopab1  3971  cbvopab2  3972  cbvopab1s  3973  cbvopab2v  3975  unopab  3977  opabid  4149  elopab  4150  ssopab2  4167  iunopab  4173  elxpi  4525  rabxp  4546  csbxpg  4590  relopabi  4635  opabbrex  5783  dfoprab2  5786  dmoprab  5820  dfopab2  6055  cnvoprab  6099
  Copyright terms: Public domain W3C validator