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

Definition df-rab 2362
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 2357 . 2  class  { x  e.  A  |  ph }
52cv 1284 . . . . 5  class  x
65, 3wcel 1434 . . . 4  wff  x  e.  A
76, 1wa 102 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cab 2069 . 2  class  { x  |  ( x  e.  A  /\  ph ) }
94, 8wceq 1285 1  wff  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
Colors of variables: wff set class
This definition is referenced by:  rabid  2534  rabid2  2535  rabbi  2536  rabswap  2537  nfrab1  2538  nfrabxy  2539  rabbiia  2596  rabeqf  2600  cbvrab  2608  rabab  2629  elrabi  2754  elrabf  2755  elrab3t  2756  ralrab2  2766  rexrab2  2768  cbvrabcsf  2976  dfin5  2989  dfdif2  2990  ss2rab  3079  rabss  3080  ssrab  3081  rabss2  3086  ssrab2  3088  rabssab  3090  notab  3250  unrab  3251  inrab  3252  inrab2  3253  difrab  3254  dfrab2  3255  dfrab3  3256  notrab  3257  rabun2  3259  dfnul3  3270  rabn0r  3287  rabn0m  3288  rab0  3289  rabeq0  3290  dfif6  3370  rabsn  3477  reusn  3481  rabsneu  3483  elunirab  3634  elintrab  3668  ssintrab  3679  iunrab  3745  iinrabm  3760  intexrabim  3948  repizf2  3956  exss  4010  rabxp  4426  exse2  4749  mptpreima  4864  fndmin  5326  fncnvima2  5340  riotauni  5525  riotacl2  5532  snriota  5548  xp2  5850  unielxp  5851  dfopab2  5866  unfiexmid  6462  nnzrab  8508  nn0zrab  8509  shftlem  9905  shftuz  9906  shftdm  9911  negfi  10311  bdcrab  10910
  Copyright terms: Public domain W3C validator