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

Definition df-rab 2309
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 2304 . 2 class {x Aφ}
52cv 1241 . . . . 5 class x
65, 3wcel 1390 . . . 4 wff x A
76, 1wa 97 . . 3 wff (x A φ)
87, 2cab 2023 . 2 class {x ∣ (x A φ)}
94, 8wceq 1242 1 wff {x Aφ} = {x ∣ (x A φ)}
Colors of variables: wff set class
This definition is referenced by:  rabid  2479  rabid2  2480  rabbi  2481  rabswap  2482  nfrab1  2483  nfrabxy  2484  rabbiia  2541  rabeqf  2544  cbvrab  2549  rabab  2569  elrabi  2689  elrabf  2690  elrab3t  2691  ralrab2  2700  rexrab2  2702  cbvrabcsf  2905  dfin5  2919  dfdif2  2920  ss2rab  3010  rabss  3011  ssrab  3012  rabss2  3017  ssrab2  3019  rabssab  3021  notab  3201  unrab  3202  inrab  3203  inrab2  3204  difrab  3205  dfrab2  3206  dfrab3  3207  notrab  3208  rabun2  3210  dfnul3  3221  rabn0r  3238  rabn0m  3239  rab0  3240  rabeq0  3241  dfif6  3327  rabsn  3428  reusn  3432  rabsneu  3434  elunirab  3584  elintrab  3618  ssintrab  3629  iunrab  3695  iinrabm  3710  intexrabim  3898  repizf2  3906  exss  3954  rabxp  4323  exse2  4642  mptpreima  4757  fndmin  5217  fncnvima2  5231  riotauni  5417  riotacl2  5424  snriota  5440  xp2  5741  unielxp  5742  dfopab2  5757  nnzrab  8025  nn0zrab  8026  bdcrab  9287
  Copyright terms: Public domain W3C validator