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

Definition df-opab 4426
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 4711 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 6753. For example,  R  =  { <. x ,  y >.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 25274). (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 4424 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  setvar  z
65cv 1398 . . . . . . 7  class  z
72cv 1398 . . . . . . . 8  class  x
83cv 1398 . . . . . . . 8  class  y
97, 8cop 3950 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1399 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 367 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1620 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1620 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2367 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1399 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  4428  opabbid  4429  nfopab  4432  nfopab1  4433  nfopab2  4434  cbvopab  4435  cbvopab1  4437  cbvopab2  4438  cbvopab1s  4439  cbvopab2v  4441  unopab  4442  opabid  4668  elopab  4669  ssopab2  4687  iunopab  4697  dfid3  4710  elxpi  4929  rabxp  4950  csbxp  4995  relopabi  5040  opabbrexOLD  6239  dfoprab2  6242  dmoprab  6282  opabex2  6637  dfopab2  6753  brdom7disj  8822  brdom6disj  8823  cnvoprab  27696  areacirc  30278  dropab1  31524  dropab2  31525  csbxpgOLD  33964  csbxpgVD  34041  relopabVD  34048
  Copyright terms: Public domain W3C validator