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

Definition df-rab 2402
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 2397 . 2 class {𝑥𝐴𝜑}
52cv 1315 . . . . 5 class 𝑥
65, 3wcel 1465 . . . 4 wff 𝑥𝐴
76, 1wa 103 . . 3 wff (𝑥𝐴𝜑)
87, 2cab 2103 . 2 class {𝑥 ∣ (𝑥𝐴𝜑)}
94, 8wceq 1316 1 wff {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
Colors of variables: wff set class
This definition is referenced by:  rabid  2583  rabid2  2584  rabbi  2585  rabswap  2586  nfrab1  2587  nfrabxy  2588  rabbiia  2645  rabbidva2  2647  rabeqf  2650  cbvrab  2658  rabab  2681  elrabi  2810  elrabf  2811  elrab3t  2812  ralrab2  2822  rexrab2  2824  cbvrabcsf  3035  dfin5  3048  dfdif2  3049  ss2rab  3143  rabss  3144  ssrab  3145  rabss2  3150  ssrab2  3152  rabssab  3154  notab  3316  unrab  3317  inrab  3318  inrab2  3319  difrab  3320  dfrab2  3321  dfrab3  3322  notrab  3323  rabun2  3325  dfnul3  3336  rabn0r  3359  rabn0m  3360  rab0  3361  rabeq0  3362  dfif6  3446  rabsn  3560  reusn  3564  rabsneu  3566  elunirab  3719  elintrab  3753  ssintrab  3764  iunrab  3830  iinrabm  3845  intexrabim  4048  repizf2  4056  exss  4119  rabxp  4546  exse2  4883  mptpreima  5002  fndmin  5495  fncnvima2  5509  riotauni  5704  riotacl2  5711  snriota  5727  xp2  6039  unielxp  6040  dfopab2  6055  unfiexmid  6774  nnzrab  9036  nn0zrab  9037  shftlem  10543  shftuz  10544  shftdm  10549  negfi  10954  cnblcld  12615  bdcrab  12946
  Copyright terms: Public domain W3C validator