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

Definition df-opab 4483
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 4771 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 6861. For example,  R  =  { <. x ,  y >.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 25880). (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 4481 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  setvar  z
65cv 1436 . . . . . . 7  class  z
72cv 1436 . . . . . . . 8  class  x
83cv 1436 . . . . . . . 8  class  y
97, 8cop 4004 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1437 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 370 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1657 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1657 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2407 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1437 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  4485  opabbid  4486  nfopab  4489  nfopab1  4490  nfopab2  4491  cbvopab  4492  cbvopab1  4494  cbvopab2  4495  cbvopab1s  4496  cbvopab2v  4498  unopab  4499  opabid  4727  elopab  4728  ssopab2  4746  iunopab  4756  dfid3  4769  elxpi  4869  rabxp  4890  csbxp  4935  relopabi  4978  opabbrexOLD  6348  dfoprab2  6351  dmoprab  6391  opabex2  6745  dfopab2  6861  brdom7disj  8966  brdom6disj  8967  cnvoprab  28314  areacirc  32001  dropab1  36770  dropab2  36771  csbxpgOLD  37187  csbxpgVD  37264  relopabVD  37271
  Copyright terms: Public domain W3C validator