ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-rab Unicode version

Definition df-rab 2464
Description: Define a restricted class abstraction (class builder), which is the class of all  x in  A such that  ph is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
df-rab  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }

Detailed syntax breakdown of Definition df-rab
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  setvar  x
3 cA . . 3  class  A
41, 2, 3crab 2459 . 2  class  { x  e.  A  |  ph }
52cv 1352 . . . . 5  class  x
65, 3wcel 2148 . . . 4  wff  x  e.  A
76, 1wa 104 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cab 2163 . 2  class  { x  |  ( x  e.  A  /\  ph ) }
94, 8wceq 1353 1  wff  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
Colors of variables: wff set class
This definition is referenced by:  rabid  2652  rabid2  2653  rabbi  2654  rabswap  2655  nfrab1  2656  nfrabxy  2657  rabbiia  2722  rabbidva2  2724  rabeqf  2727  cbvrab  2735  rabab  2758  elrabi  2890  elrabf  2891  elrab3t  2892  ralrab2  2902  rexrab2  2904  cbvrabcsf  3122  dfin5  3136  dfdif2  3137  ss2rab  3231  rabss  3232  ssrab  3233  rabss2  3238  ssrab2  3240  rabssab  3243  notab  3405  unrab  3406  inrab  3407  inrab2  3408  difrab  3409  dfrab2  3410  dfrab3  3411  notrab  3412  rabun2  3414  dfnul3  3425  rabn0r  3449  rabn0m  3450  rab0  3451  rabeq0  3452  dfif6  3536  rabsn  3658  reusn  3662  rabsneu  3664  elunirab  3820  elintrab  3854  ssintrab  3865  iunrab  3931  iinrabm  3946  intexrabim  4150  repizf2  4159  exss  4223  rabxp  4659  exse2  4997  mptpreima  5117  fndmin  5618  fncnvima2  5632  riotauni  5830  riotacl2  5837  snriota  5853  xp2  6167  unielxp  6168  dfopab2  6183  unfiexmid  6910  nnzrab  9253  nn0zrab  9254  shftlem  10796  shftuz  10797  shftdm  10802  negfi  11207  cnblcld  13668  if0ab  14179  bdcrab  14226
  Copyright terms: Public domain W3C validator