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

Definition df-opab 3846
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 3844 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  setvar  z
65cv 1258 . . . . . . 7  class  z
72cv 1258 . . . . . . . 8  class  x
83cv 1258 . . . . . . . 8  class  y
97, 8cop 3405 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1259 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 101 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1397 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1397 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2042 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1259 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  3848  opabbid  3849  nfopab  3852  nfopab1  3853  nfopab2  3854  cbvopab  3855  cbvopab1  3857  cbvopab2  3858  cbvopab1s  3859  cbvopab2v  3861  unopab  3863  opabid  4021  elopab  4022  ssopab2  4039  iunopab  4045  elxpi  4388  rabxp  4407  csbxpg  4448  relopabi  4490  opabbrex  5576  dfoprab2  5579  dmoprab  5612  dfopab2  5842  cnvoprab  5882
  Copyright terms: Public domain W3C validator