Definition df-rab 2802

Description: Define a restricted class abstraction (class builder), which is the class of all x in A such that ph is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)

Assertion

Ref	Expression
df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }

Detailed syntax breakdown of Definition df-rab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	crab 2797	. 2 class { x e. A | ph }
5	2	cv 1382	. . . . 5 class x
6	5, 3	wcel 1804	. . . 4 wff x e. A
7	6, 1	wa 369	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2428	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1383	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  3020  rabid2  3021  rabbi  3022  rabswap  3023  nfrab1  3024  nfrab  3025  rabbiia  3084  rabbidva2  3085  rabeqf  3088  cbvrab  3093  rabab  3113  elrabi  3240  elrabf  3241  elrab3t  3242  ralrab2  3251  rexrab2  3253  cbvrabcsf  3455  dfin5  3469  dfdif2  3470  ss2rab  3561  rabss  3562  ssrab  3563  rabss2  3568  ssrab2  3570  rabssab  3572  notab  3753  unrab  3754  inrab  3755  inrab2  3756  difrab  3757  dfrab3  3758  notrab  3760  rabun2  3762  dfnul3  3773  rabn0  3791  rab0  3792  dfif6  3929  rabsn  4082  rabsnifsb  4083  reusn  4088  rabsneu  4090  elunirab  4246  elintrab  4283  ssintrab  4295  rabasiun  4319  iunrab  4362  iinrab  4377  intexrab  4596  rmorabex  4697  exss  4700  rabxp  5026  mptpreima  5490  fndmin  5979  fncnvima2  5994  riotauni  6248  riotacl2  6256  snriota  6272  orduniss2  6653  exse2  6724  zfrep6  6753  xp2  6820  unielxp  6821  dfopab2  6839  suppvalbr  6907  ressuppss  6921  rankval3b  8247  scottexs  8308  scott0s  8309  kardex  8315  cardval2  8375  r0weon  8393  axdc2lem  8831  sstskm  9223  nnzrab  10899  nn0zrab  10900  wrdnval  12553  cshwsexa  12774  shftlem  12883  shftuz  12884  shftdm  12886  hashbc0  14505  cshwsiun  14566  submacs  15975  cycsubg  16208  eqglact  16231  dfrhm2  17345  aspval2  17975  psrbaglefi  18002  psrbaglefiOLD  18003  znunithash  18581  clsval2  19529  xkoptsub  20133  ptcmplem2  20531  cnblcld  21260  cncmet  21739  shft2rab  21897  sca2rab  21901  vmappw  23368  usgraop  24328  nbgraf1olem5  24423  nb3graprlem1  24429  wwlknprop  24664  wwlknfi  24716  wlknwwlknvbij  24718  clwwlkvbij  24779  eclclwwlkn1  24810  vdgrun  24879  vdgrfiun  24880  rusgranumwlkb0  24931  rusgra0edg  24933  h2hcau  25874  dfch2  26303  hhcno  26801  hhcnf  26802  pjhmopidm  27080  elpjrn  27087  rabrab  27377  rabid2f  27378  rabfmpunirn  27469  mptctf  27522  maprnin  27532  fpwrelmapffslem  27533  fpwrelmap  27534  sigaex  28087  sigaval  28088  isrnsigaOLD  28090  ballotlem2  28405  setlikespec  29243  rabiun  30012  ptrest  30024  cnambfre  30039  areacirclem5  30087  neibastop3  30156  ispridlc  30443  eq0rabdioph  30686  rexrabdioph  30703  eldioph4b  30721  aomclem4  30979  rabexgf  31353  submgmacs  32446  rabeqsn  32787  rabsssn  32788  bnj1441  33767  bnj110  33784  bj-rababwv  34326  bj-rabbida2  34368  bj-inrab  34378  lkrval2  34690  lfl1dim  34721  glbconxN  34977  dva1dim  36586  dib1dim2  36770  diclspsn  36796  dih1dimatlem  36931  dihglb2  36944  hdmapoc  37536