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

Definition df-rab 2426
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 2421 . 2 class {𝑥𝐴𝜑}
52cv 1331 . . . . 5 class 𝑥
65, 3wcel 1481 . . . 4 wff 𝑥𝐴
76, 1wa 103 . . 3 wff (𝑥𝐴𝜑)
87, 2cab 2126 . 2 class {𝑥 ∣ (𝑥𝐴𝜑)}
94, 8wceq 1332 1 wff {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
Colors of variables: wff set class
This definition is referenced by:  rabid  2609  rabid2  2610  rabbi  2611  rabswap  2612  nfrab1  2613  nfrabxy  2614  rabbiia  2674  rabbidva2  2676  rabeqf  2679  cbvrab  2687  rabab  2710  elrabi  2840  elrabf  2841  elrab3t  2842  ralrab2  2852  rexrab2  2854  cbvrabcsf  3069  dfin5  3082  dfdif2  3083  ss2rab  3177  rabss  3178  ssrab  3179  rabss2  3184  ssrab2  3186  rabssab  3188  notab  3350  unrab  3351  inrab  3352  inrab2  3353  difrab  3354  dfrab2  3355  dfrab3  3356  notrab  3357  rabun2  3359  dfnul3  3370  rabn0r  3393  rabn0m  3394  rab0  3395  rabeq0  3396  dfif6  3480  rabsn  3597  reusn  3601  rabsneu  3603  elunirab  3756  elintrab  3790  ssintrab  3801  iunrab  3867  iinrabm  3882  intexrabim  4085  repizf2  4093  exss  4156  rabxp  4583  exse2  4920  mptpreima  5039  fndmin  5534  fncnvima2  5548  riotauni  5743  riotacl2  5750  snriota  5766  xp2  6078  unielxp  6079  dfopab2  6094  unfiexmid  6813  nnzrab  9101  nn0zrab  9102  shftlem  10619  shftuz  10620  shftdm  10625  negfi  11030  cnblcld  12741  bdcrab  13219
  Copyright terms: Public domain W3C validator