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

Definition df-rab 2289
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 2284 . 2 class {x Aφ}
52cv 1225 . . . . 5 class x
65, 3wcel 1370 . . . 4 wff x A
76, 1wa 97 . . 3 wff (x A φ)
87, 2cab 2004 . 2 class {x ∣ (x A φ)}
94, 8wceq 1226 1 wff {x Aφ} = {x ∣ (x A φ)}
Colors of variables: wff set class
This definition is referenced by:  rabid  2459  rabid2  2460  rabbi  2461  rabswap  2462  nfrab1  2463  nfrabxy  2464  rabbiia  2521  rabeqf  2524  cbvrab  2529  rabab  2548  elrabi  2668  elrabf  2669  elrab3t  2670  ralrab2  2679  rexrab2  2681  cbvrabcsf  2884  dfin5  2898  dfdif2  2899  ss2rab  2989  rabss  2990  ssrab  2991  rabss2  2996  ssrab2  2998  rabssab  3000  notab  3180  unrab  3181  inrab  3182  inrab2  3183  difrab  3184  dfrab2  3185  dfrab3  3186  notrab  3187  rabun2  3189  dfnul3  3200  rabn0r  3217  rabn0m  3218  rab0  3219  rabeq0  3220  dfif6  3308  rabsn  3407  reusn  3411  rabsneu  3413  elunirab  3563  elintrab  3597  ssintrab  3608  iunrab  3674  iinrabm  3689  intexrabim  3877  repizf2  3885  exss  3933  rabxp  4303  exse2  4622  mptpreima  4737  fndmin  5195  fncnvima2  5209  riotauni  5394  riotacl2  5401  snriota  5417  xp2  5718  unielxp  5719  dfopab2  5734  bdcrab  7218
  Copyright terms: Public domain W3C validator