MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-opab Structured version   Unicode version

Definition df-opab 4292
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 (see dfid2 4529 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 6430. For example,  R  =  { <. x ,  y
>.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 21771). (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  set  x
3 vy . . 3  set  y
41, 2, 3copab 4290 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  set  z
65cv 1652 . . . . . . 7  class  z
72cv 1652 . . . . . . . 8  class  x
83cv 1652 . . . . . . . 8  class  y
97, 8cop 3841 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1653 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 360 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1551 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1551 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2428 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1653 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  4294  opabbid  4295  nfopab  4298  nfopab1  4299  nfopab2  4300  cbvopab  4301  cbvopab1  4303  cbvopab2  4304  cbvopab1s  4305  cbvopab2v  4307  unopab  4309  opabid  4490  elopab  4491  ssopab2  4509  iunopab  4515  dfid3  4528  elxpi  4923  csbxpg  4934  rabxp  4943  relopabi  5029  opabbrex  6147  dfoprab2  6150  dmoprab  6183  dfopab2  6430  brdom7disj  8440  brdom6disj  8441  areacirc  26335  dropab1  27664  dropab2  27665  csbxpgVD  29104  relopabVD  29111
  Copyright terms: Public domain W3C validator