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

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

Detailed syntax breakdown of Definition df-rab
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3crab 2353 . 2 class {𝑥𝐴𝜑}
52cv 1284 . . . . 5 class 𝑥
65, 3wcel 1434 . . . 4 wff 𝑥𝐴
76, 1wa 102 . . 3 wff (𝑥𝐴𝜑)
87, 2cab 2068 . 2 class {𝑥 ∣ (𝑥𝐴𝜑)}
94, 8wceq 1285 1 wff {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
Colors of variables: wff set class
This definition is referenced by:  rabid  2530  rabid2  2531  rabbi  2532  rabswap  2533  nfrab1  2534  nfrabxy  2535  rabbiia  2592  rabeqf  2595  cbvrab  2600  rabab  2621  elrabi  2747  elrabf  2748  elrab3t  2749  ralrab2  2758  rexrab2  2760  cbvrabcsf  2968  dfin5  2981  dfdif2  2982  ss2rab  3071  rabss  3072  ssrab  3073  rabss2  3078  ssrab2  3080  rabssab  3082  notab  3241  unrab  3242  inrab  3243  inrab2  3244  difrab  3245  dfrab2  3246  dfrab3  3247  notrab  3248  rabun2  3250  dfnul3  3261  rabn0r  3278  rabn0m  3279  rab0  3280  rabeq0  3281  dfif6  3361  rabsn  3467  reusn  3471  rabsneu  3473  elunirab  3622  elintrab  3656  ssintrab  3667  iunrab  3733  iinrabm  3748  intexrabim  3936  repizf2  3944  exss  3990  rabxp  4406  exse2  4729  mptpreima  4844  fndmin  5306  fncnvima2  5320  riotauni  5505  riotacl2  5512  snriota  5528  xp2  5830  unielxp  5831  dfopab2  5846  unfiexmid  6438  nnzrab  8456  nn0zrab  8457  shftlem  9842  shftuz  9843  shftdm  9848  negfi  10248  bdcrab  10801
  Copyright terms: Public domain W3C validator