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

Definition df-opab 3877
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 3875 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  setvar  z
65cv 1286 . . . . . . 7  class  z
72cv 1286 . . . . . . . 8  class  x
83cv 1286 . . . . . . . 8  class  y
97, 8cop 3434 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1287 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 102 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1424 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1424 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2071 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1287 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  3879  opabbid  3880  nfopab  3883  nfopab1  3884  nfopab2  3885  cbvopab  3886  cbvopab1  3888  cbvopab2  3889  cbvopab1s  3890  cbvopab2v  3892  unopab  3894  opabid  4060  elopab  4061  ssopab2  4078  iunopab  4084  elxpi  4429  rabxp  4448  csbxpg  4489  relopabi  4533  opabbrex  5652  dfoprab2  5655  dmoprab  5688  dfopab2  5918  cnvoprab  5958
  Copyright terms: Public domain W3C validator