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

Definition df-opab 3994
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 3992 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  setvar  z
65cv 1331 . . . . . . 7  class  z
72cv 1331 . . . . . . . 8  class  x
83cv 1331 . . . . . . . 8  class  y
97, 8cop 3531 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1332 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 103 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1469 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1469 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2126 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1332 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  3996  opabbid  3997  nfopab  4000  nfopab1  4001  nfopab2  4002  cbvopab  4003  cbvopab1  4005  cbvopab2  4006  cbvopab1s  4007  cbvopab2v  4009  unopab  4011  opabid  4183  elopab  4184  ssopab2  4201  iunopab  4207  elxpi  4559  rabxp  4580  csbxpg  4624  relopabi  4669  opabbrex  5819  dfoprab2  5822  dmoprab  5856  dfopab2  6091  cnvoprab  6135
  Copyright terms: Public domain W3C validator