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

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

Detailed syntax breakdown of Definition df-rab
StepHypRef Expression
1 wph . . 3 wff φ
2 vx . . 3 setvar x
3 cA . . 3 class A
41, 2, 3crab 2279 . 2 class {x Aφ}
52cv 1222 . . . . 5 class x
65, 3wcel 1366 . . . 4 wff x A
76, 1wa 97 . . 3 wff (x A φ)
87, 2cab 1999 . 2 class {x ∣ (x A φ)}
94, 8wceq 1223 1 wff {x Aφ} = {x ∣ (x A φ)}
Colors of variables: wff set class
This definition is referenced by:  rabid  2454  rabid2  2455  rabbi  2456  rabswap  2457  nfrab1  2458  nfrabxy  2459  rabbiia  2516  rabeqf  2519  cbvrab  2524  rabab  2543  elrabi  2663  elrabf  2664  elrab3t  2665  ralrab2  2674  rexrab2  2676  cbvrabcsf  2879  dfin5  2893  dfdif2  2894  ss2rab  2984  rabss  2985  ssrab  2986  rabss2  2991  ssrab2  2993  rabssab  2995  notab  3175  unrab  3176  inrab  3177  inrab2  3178  difrab  3179  dfrab2  3180  dfrab3  3181  notrab  3182  rabun2  3184  dfnul3  3195  rabn0r  3212  rabn0m  3213  rab0  3214  rabeq0  3215  dfif6  3301  rabsn  3400  reusn  3404  rabsneu  3406  elunirab  3556  elintrab  3590  ssintrab  3601  iunrab  3667  iinrabm  3682  intexrabim  3870  repizf2  3878  exss  3926  rabxp  4295  exse2  4614  mptpreima  4729  fndmin  5187  fncnvima2  5201  riotauni  5386  riotacl2  5393  snriota  5409  xp2  5710  unielxp  5711  dfopab2  5726  nnzrab  7843  nn0zrab  7844  bdcrab  8237
  Copyright terms: Public domain W3C validator