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

Definition df-opab 4501
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 4792 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 6830. For example,  R  =  { <. x ,  y
>.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 24818). (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 4499 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  setvar  z
65cv 1373 . . . . . . 7  class  z
72cv 1373 . . . . . . . 8  class  x
83cv 1373 . . . . . . . 8  class  y
97, 8cop 4028 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1374 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 369 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1591 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1591 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2447 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1374 1  wff  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
Colors of variables: wff setvar class
This definition is referenced by:  opabss  4503  opabbid  4504  nfopab  4507  nfopab1  4508  nfopab2  4509  cbvopab  4510  cbvopab1  4512  cbvopab2  4513  cbvopab1s  4514  cbvopab2v  4516  unopab  4517  opabid  4749  elopab  4750  ssopab2  4768  iunopab  4778  dfid3  4791  elxpi  5010  rabxp  5030  csbxp  5074  csbxpgOLD  5075  relopabi  5121  opabbrex  6317  dfoprab2  6320  dmoprab  6360  opabex2  6714  dfopab2  6830  brdom7disj  8900  brdom6disj  8901  swrd0  12610  cnvoprab  27206  areacirc  29678  dropab1  30891  dropab2  30892  csbxpgVD  32651  relopabVD  32658
  Copyright terms: Public domain W3C validator