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

Definition df-rab 2315
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 2310 . 2  class  { x  e.  A  |  ph }
52cv 1242 . . . . 5  class  x
65, 3wcel 1393 . . . 4  wff  x  e.  A
76, 1wa 97 . . 3  wff  ( x  e.  A  /\  ph )
87, 2cab 2026 . 2  class  { x  |  ( x  e.  A  /\  ph ) }
94, 8wceq 1243 1  wff  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
Colors of variables: wff set class
This definition is referenced by:  rabid  2485  rabid2  2486  rabbi  2487  rabswap  2488  nfrab1  2489  nfrabxy  2490  rabbiia  2547  rabeqf  2550  cbvrab  2555  rabab  2575  elrabi  2695  elrabf  2696  elrab3t  2697  ralrab2  2706  rexrab2  2708  cbvrabcsf  2911  dfin5  2925  dfdif2  2926  ss2rab  3016  rabss  3017  ssrab  3018  rabss2  3023  ssrab2  3025  rabssab  3027  notab  3207  unrab  3208  inrab  3209  inrab2  3210  difrab  3211  dfrab2  3212  dfrab3  3213  notrab  3214  rabun2  3216  dfnul3  3227  rabn0r  3244  rabn0m  3245  rab0  3246  rabeq0  3247  dfif6  3333  rabsn  3437  reusn  3441  rabsneu  3443  elunirab  3593  elintrab  3627  ssintrab  3638  iunrab  3704  iinrabm  3719  intexrabim  3907  repizf2  3915  exss  3963  rabxp  4380  exse2  4699  mptpreima  4814  fndmin  5274  fncnvima2  5288  riotauni  5474  riotacl2  5481  snriota  5497  xp2  5799  unielxp  5800  dfopab2  5815  nnzrab  8269  nn0zrab  8270  shftlem  9417  shftuz  9418  shftdm  9423  bdcrab  9972
  Copyright terms: Public domain W3C validator