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

Definition df-opab 4049
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 4047 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  setvar  z
65cv 1347 . . . . . . 7  class  z
72cv 1347 . . . . . . . 8  class  x
83cv 1347 . . . . . . . 8  class  y
97, 8cop 3584 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1348 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 103 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1485 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1485 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2156 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1348 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  4051  opabbid  4052  nfopab  4055  nfopab1  4056  nfopab2  4057  cbvopab  4058  cbvopab1  4060  cbvopab2  4061  cbvopab1s  4062  cbvopab2v  4064  unopab  4066  opabid  4240  elopab  4241  ssopab2  4258  iunopab  4264  elxpi  4625  rabxp  4646  csbxpg  4690  relopabi  4735  opabbrex  5894  dfoprab2  5897  dmoprab  5931  dfopab2  6165  cnvoprab  6210
  Copyright terms: Public domain W3C validator