Definition df-rab 3415

Description: Define a restricted class abstraction (class builder): {𝑥 ∈ 𝐴 ∣ 𝜑} is the class of all sets 𝑥 in 𝐴 such that 𝜑(𝑥) is true. Definition of [TakeutiZaring] p. 20.

For the interpretation given in the previous paragraph to be correct, we need to assume Ⅎ𝑥𝐴, which is the case as soon as 𝑥 and 𝐴 are disjoint, which is generally the case. If 𝐴 were to depend on 𝑥, then the interpretation would be less obvious (think of the two extreme cases 𝐴 = {𝑥} and 𝐴 = 𝑥, for instance). See also df-ral 3079. (Contributed by NM, 22-Nov-1994.)

Assertion

Ref	Expression
df-rab	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

Detailed syntax breakdown of Definition df-rab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	crab 3414	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1569	. . . . 5 class 𝑥
6	5, 3	wcel 2145	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2740	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1570	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is used by:  rabbidva2  3416  cbvrabv  3424  rabeqcda  3425  rabrabi  3433  nfrab1  3434  rabid  3435  rabbida4  3439  rabbi  3444  rabid2f  3445  rabid2im  3446  cbvrabw  3449  nfrabw  3450  nfrab  3451  cbvrab  3452  rabab  3483  elrabi  3644  elrabf  3645  elrab3t  3647  elrab  3648  elrab2w  3653  ralrab2  3659  rexrab2  3661  cbvrabcsfw  3891  cbvrabcsf  3895  dfin5  3910  dfdif2  3911  ss2rab  4020  rabss  4021  ssrab  4022  ss2rabd  4023  rabss2  4028  rabss2OLD  4029  rabssab  4036  notab  4263  unrab  4264  inrab  4265  inrab2  4266  difrab  4267  dfrab3  4268  notrab  4271  rabun2  4273  dfnul3  4286  rab0OLD  4339  rabeq0w  4340  rabeq0  4341  dfif6  4488  rabeqsn  4631  rabsssn  4632  rabsnifsb  4686  reusn  4691  rabsneu  4693  elunirab  4885  elintrab  4923  ssintrab  4934  iunrab  5015  iinrab  5031  intexrab  5315  rmorabex  5439  exss  5442  rabxp  5707  mptpreima  6238  setlikespec  6327  predres  6341  fndmin  7041  fncnvima2  7057  riotauni  7380  riotacl2  7390  snriota  7407  orduniss2  7833  exse2  7918  zfrep6OLD  7956  xp2  8027  unielxp  8028  dfopab2  8053  suppvalbr  8166  ressuppss  8185  rankval3b  9812  scottabf  9882  scottexsOLD  9886  scott0bsOLD  9888  kardexOLD  9901  cardval2  10000  r0weon  10019  axdc2lem  10454  sstskm  10855  negfi  12192  nnzrab  12650  nn0zrab  12651  prprrab  14542  wrdnval  14614  shftlem  15145  shftuz  15146  shftdm  15148  hashbc0  17103  cshwsiun  17197  nfchnd  18705  submgmacs  18825  submacs  18942  eqglact  19310  cycsubg  19342  dfrhm2  20621  znunithash  21783  aspval2  22119  psrbaglefi  22147  clsval2  23281  xkoptsub  23886  ptcmplem2  24285  cnblcld  25006  cncmet  25556  shft2rab  25742  sca2rab  25746  vmappw  27360  2lgslem1b  27636  madeval2  28106  nb3grprlem1  29848  vtxdun  29949  rusgrprc  30058  ewlksfval  30069  wwlksnfi  30382  rusgrnumwwlkb0  30450  eclclwwlkn1  30553  clwwlkvbij  30591  h2hcau  31468  dfch2  31896  hhcno  32393  hhcnf  32394  pjhmopidm  32672  elpjrn  32679  dmrab  32980  rabsspr  32984  rabsstp  32985  rabfmpunirn  33134  mptctf  33195  maprnin  33210  fpwrelmapffslem  33211  fpwrelmap  33212  sigaex  34628  sigaval  34629  bnj1441  35357  bnj1441g  35358  bnj110  35375  fnrelpredd  35604  rabeqbii  36822  cbvrabdavw  36889  cbvrabdavw2  36913  neibastop3  36989  bj-rababw  37632  bj-inrab  37679  rabiun  38360  ptrest  38376  poimirlem26  38403  poimirlem27  38404  cnambfre  38425  areacirclem5  38469  ispridlc  38828  eqrabi  39012  ec1cnvres  39032  eccnvepres  39042  lkrval2  39971  lfl1dim  40002  glbconxN  40259  dva1dim  41866  dib1dim2  42049  diclspsn  42075  dih1dimatlem  42210  dihglb2  42223  hdmapoc  42812  sticksstones23  43043  aks6d1c6isolem3  43050  prjspeclsp  43466  eq0rabdioph  43629  rexrabdioph  43643  eldioph4b  43660  aomclem4  43906  onsucrn  44120  dfno2  44276  harval3  44386  alephiso2  44406  clcnvlem  44471  ntrneiel2  44934  rabexgf  45866  ssrabf  45954  rabssf  45959  cbvrabv2w  45968  rabbida2  45972  rabbida3  45975  f1oresf1o  48186  sprvalpw  48388  prprvalpw  48423  prprspr2  48426  stgr1  48885  dfnrm2  49866  dfnrm3  49867