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

Definition df-opab 4077
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 4075 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  setvar  z
65cv 1362 . . . . . . 7  class  z
72cv 1362 . . . . . . . 8  class  x
83cv 1362 . . . . . . . 8  class  y
97, 8cop 3607 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1363 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 104 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1502 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1502 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2173 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1363 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  4079  opabbid  4080  nfopab  4083  nfopab1  4084  nfopab2  4085  cbvopab  4086  cbvopab1  4088  cbvopab2  4089  cbvopab1s  4090  cbvopab2v  4092  unopab  4094  opabid  4269  elopab  4270  ssopab2  4287  iunopab  4293  elxpi  4654  rabxp  4675  csbxpg  4719  relopabi  4764  opabbrex  5932  dfoprab2  5935  dmoprab  5969  dfopab2  6204  cnvoprab  6249
  Copyright terms: Public domain W3C validator