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

Definition df-opab 3861
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 3859 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  setvar  z
65cv 1284 . . . . . . 7  class  z
72cv 1284 . . . . . . . 8  class  x
83cv 1284 . . . . . . . 8  class  y
97, 8cop 3420 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1285 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 102 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1422 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1422 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2069 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1285 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  3863  opabbid  3864  nfopab  3867  nfopab1  3868  nfopab2  3869  cbvopab  3870  cbvopab1  3872  cbvopab2  3873  cbvopab1s  3874  cbvopab2v  3876  unopab  3878  opabid  4041  elopab  4042  ssopab2  4059  iunopab  4065  elxpi  4408  rabxp  4427  csbxpg  4468  relopabi  4512  opabbrex  5602  dfoprab2  5605  dmoprab  5638  dfopab2  5868  cnvoprab  5908
  Copyright terms: Public domain W3C validator