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

Definition df-opab 4235
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 4468 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 6368. For example,  R  =  { <. x ,  y
>.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 21701). (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 4233 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  set  z
65cv 1648 . . . . . . 7  class  z
72cv 1648 . . . . . . . 8  class  x
83cv 1648 . . . . . . . 8  class  y
97, 8cop 3785 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1649 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 359 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1547 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1547 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2398 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1649 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  4237  opabbid  4238  nfopab  4241  nfopab1  4242  nfopab2  4243  cbvopab  4244  cbvopab1  4246  cbvopab2  4247  cbvopab1s  4248  cbvopab2v  4250  unopab  4252  opabid  4429  elopab  4430  ssopab2  4448  iunopab  4454  dfid3  4467  elxpi  4861  csbxpg  4872  rabxp  4881  relopabi  4967  opabbrex  6085  dfoprab2  6088  dmoprab  6121  dfopab2  6368  brdom7disj  8373  brdom6disj  8374  areacirc  26195  dropab1  27525  dropab2  27526  csbxpgVD  28724  relopabVD  28731
  Copyright terms: Public domain W3C validator