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

Definition df-rab 2384
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 2379 . 2  class  { x  e.  A  |  ph }
52cv 1298 . . . . 5  class  x
65, 3wcel 1448 . . . 4  wff  x  e.  A
76, 1wa 103 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cab 2086 . 2  class  { x  |  ( x  e.  A  /\  ph ) }
94, 8wceq 1299 1  wff  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
Colors of variables: wff set class
This definition is referenced by:  rabid  2564  rabid2  2565  rabbi  2566  rabswap  2567  nfrab1  2568  nfrabxy  2569  rabbiia  2626  rabbidva2  2628  rabeqf  2631  cbvrab  2639  rabab  2662  elrabi  2790  elrabf  2791  elrab3t  2792  ralrab2  2802  rexrab2  2804  cbvrabcsf  3015  dfin5  3028  dfdif2  3029  ss2rab  3120  rabss  3121  ssrab  3122  rabss2  3127  ssrab2  3129  rabssab  3131  notab  3293  unrab  3294  inrab  3295  inrab2  3296  difrab  3297  dfrab2  3298  dfrab3  3299  notrab  3300  rabun2  3302  dfnul3  3313  rabn0r  3336  rabn0m  3337  rab0  3338  rabeq0  3339  dfif6  3423  rabsn  3537  reusn  3541  rabsneu  3543  elunirab  3696  elintrab  3730  ssintrab  3741  iunrab  3807  iinrabm  3822  intexrabim  4018  repizf2  4026  exss  4087  rabxp  4514  exse2  4849  mptpreima  4968  fndmin  5459  fncnvima2  5473  riotauni  5668  riotacl2  5675  snriota  5691  xp2  6001  unielxp  6002  dfopab2  6017  unfiexmid  6735  nnzrab  8930  nn0zrab  8931  shftlem  10429  shftuz  10430  shftdm  10435  negfi  10838  cnblcld  12457  bdcrab  12631
  Copyright terms: Public domain W3C validator