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

Definition df-opab 3930
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 3928 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  setvar  z
65cv 1298 . . . . . . 7  class  z
72cv 1298 . . . . . . . 8  class  x
83cv 1298 . . . . . . . 8  class  y
97, 8cop 3477 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1299 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 103 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1436 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1436 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2086 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1299 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  3932  opabbid  3933  nfopab  3936  nfopab1  3937  nfopab2  3938  cbvopab  3939  cbvopab1  3941  cbvopab2  3942  cbvopab1s  3943  cbvopab2v  3945  unopab  3947  opabid  4117  elopab  4118  ssopab2  4135  iunopab  4141  elxpi  4493  rabxp  4514  csbxpg  4558  relopabi  4603  opabbrex  5747  dfoprab2  5750  dmoprab  5784  dfopab2  6017  cnvoprab  6061
  Copyright terms: Public domain W3C validator