Definition df-rab 2675

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 set x
3		cA	. . 3 class A
4	1, 2, 3	crab 2670	. 2 class { x e. A | ph }
5	2	cv 1648	. . . . 5 class x
6	5, 3	wcel 1721	. . . 4 wff x e. A
7	6, 1	wa 359	. . 3 wff ( x e. A /\ ph )
8	7, 2	cab 2390	. 2 class { x | ( x e. A /\ ph ) }
9	4, 8	wceq 1649	1 wff { x e. A | ph } = { x | ( x e. A /\ ph ) }

This definition is referenced by:  rabid  2844  rabid2  2845  rabbi  2846  rabswap  2847  nfrab1  2848  nfrab  2849  rabbiia  2906  rabeqf  2909  cbvrab  2914  rabab  2933  elrabi  3050  elrabf  3051  ralrab2  3060  rexrab2  3062  cbvrabcsf  3274  dfin5  3288  dfdif2  3289  ss2rab  3379  rabss  3380  ssrab  3381  rabss2  3386  ssrab2  3388  rabssab  3390  notab  3571  unrab  3572  inrab  3573  inrab2  3574  difrab  3575  dfrab2  3576  dfrab3  3577  notrab  3578  rabun2  3580  dfnul3  3591  rabn0  3607  rab0  3608  dfif6  3702  rabsn  3833  reusn  3837  rabsneu  3839  elunirab  3988  elintrab  4022  ssintrab  4033  iunrab  4098  iinrab  4113  intexrab  4319  rmorabex  4383  exss  4386  orduniss2  4772  rabxp  4873  exse2  5197  mptpreima  5322  fndmin  5796  fncnvima2  5811  zfrep6  5927  xp2  6343  unielxp  6344  dfopab2  6360  riotauni  6515  riotacl2  6522  snriota  6539  cantnfreslem  7587  rankval3b  7708  scottexs  7767  scott0s  7768  kardex  7774  cardval2  7834  r0weon  7850  dfac2a  7966  axdc2lem  8284  sstskm  8673  nnzrab  10265  nn0zrab  10266  hashbclem  11656  shftlem  11838  shftuz  11839  shftdm  11841  hashbc0  13328  submacs  14720  cycsubg  14923  eqglact  14946  dfrhm2  15776  aspval2  16360  psrbaglefi  16392  znunithash  16800  clsval2  17069  xkoptsub  17639  ptcmplem2  18037  cnblcld  18762  cncmet  19228  shft2rab  19357  sca2rab  19361  vmappw  20852  isusgra0  21329  nbgraf1olem5  21408  nb3graprlem1  21413  vdgrun  21625  vdgrfiun  21626  h2hcau  22435  dfch2  22862  hhcno  23360  hhcnf  23361  pjhmopidm  23639  elpjrn  23646  rabid2f  23920  rabbidva2  23939  rabfmpunirn  24018  mptctf  24065  sigaex  24445  sigaval  24446  isrnsigaOLD  24448  ballotlem2  24699  setlikespec  25401  rabiun2  26139  cnambfre  26154  areacirclem6  26186  neibastop3  26281  ispridlc  26570  eq0rabdioph  26725  rexrabdioph  26744  eldioph4b  26762  aomclem4  27022  rabexgf  27562  bnj1441  28918  bnj110  28935  lkrval2  29573  lfl1dim  29604  glbconxN  29860  dva1dim  31467  dib1dim2  31651  diclspsn  31677  dih1dimatlem  31812  dihglb2  31825  mapdvalc  32112  mapdval4N  32115  hdmapoc  32417