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 3078. (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 1567	. . . . 5 class 𝑥
6	5, 3	wcel 2141	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 400	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2739	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1568	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced 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  3645  elrabf  3646  elrab3t  3648  elrab  3649  elrab2w  3654  ralrab2  3660  rexrab2  3662  cbvrabcsfw  3893  cbvrabcsf  3897  dfin5  3912  dfdif2  3913  ss2rab  4022  rabss  4023  ssrab  4024  ss2rabd  4025  rabss2  4030  rabss2OLD  4031  rabssab  4038  notab  4266  unrab  4267  inrab  4268  inrab2  4269  difrab  4270  dfrab3  4271  notrab  4274  rabun2  4276  dfnul3  4289  rab0OLD  4342  rabeq0w  4343  rabeq0  4344  dfif6  4489  rabeqsn  4632  rabsssn  4633  rabsnifsb  4687  reusn  4692  rabsneu  4694  elunirab  4886  elintrab  4924  ssintrab  4935  iunrab  5016  iinrab  5032  intexrab  5317  rmorabex  5441  exss  5444  rabxp  5709  mptpreima  6239  setlikespec  6326  predres  6340  fndmin  7040  fncnvima2  7056  riotauni  7373  riotacl2  7383  snriota  7400  orduniss2  7828  exse2  7913  zfrep6OLD  7951  xp2  8022  unielxp  8023  dfopab2  8048  suppvalbr  8159  ressuppss  8178  rankval3b  9797  scottexs  9860  scott0s  9861  scottabf  9865  kardex  9879  cardval2  9976  r0weon  9995  axdc2lem  10431  sstskm  10826  negfi  12163  nnzrab  12621  nn0zrab  12622  prprrab  14510  wrdnval  14582  shftlem  15105  shftuz  15106  shftdm  15108  hashbc0  17064  cshwsiun  17158  nfchnd  18666  submgmacs  18774  submacs  18885  eqglact  19246  cycsubg  19278  dfrhm2  20555  znunithash  21693  aspval2  22027  psrbaglefi  22055  clsval2  23186  xkoptsub  23790  ptcmplem2  24189  cnblcld  24910  cncmet  25460  shft2rab  25646  sca2rab  25650  vmappw  27256  2lgslem1b  27532  madeval2  28002  nb3grprlem1  29696  vtxdun  29797  rusgrprc  29906  ewlksfval  29917  wwlksnfi  30221  rusgrnumwwlkb0  30289  eclclwwlkn1  30392  clwwlkvbij  30430  h2hcau  31297  dfch2  31725  hhcno  32222  hhcnf  32223  pjhmopidm  32501  elpjrn  32508  dmrab  32809  rabsspr  32813  rabsstp  32814  rabfmpunirn  32964  mptctf  33027  maprnin  33042  fpwrelmapffslem  33043  fpwrelmap  33044  sigaex  34466  sigaval  34467  bnj1441  35194  bnj1441g  35195  bnj110  35212  fnrelpredd  35448  rabeqbii  36672  cbvrabdavw  36739  cbvrabdavw2  36763  neibastop3  36839  bj-rababw  37482  bj-inrab  37529  rabiun  38210  ptrest  38236  poimirlem26  38263  poimirlem27  38264  cnambfre  38285  areacirclem5  38329  ispridlc  38687  eqrabi  38873  ec1cnvres  38893  eccnvepres  38903  lkrval2  39832  lfl1dim  39863  glbconxN  40120  dva1dim  41727  dib1dim2  41910  diclspsn  41936  dih1dimatlem  42071  dihglb2  42084  hdmapoc  42673  sticksstones23  42904  aks6d1c6isolem3  42911  prjspeclsp  43314  eq0rabdioph  43477  rexrabdioph  43491  eldioph4b  43508  aomclem4  43754  onsucrn  43968  dfno2  44124  harval3  44234  alephiso2  44254  clcnvlem  44319  ntrneiel2  44782  rabexgf  45714  ssrabf  45802  rabssf  45807  cbvrabv2w  45816  rabbida2  45820  rabbida3  45823  f1oresf1o  47994  sprvalpw  48196  prprvalpw  48231  prprspr2  48234  stgr1  48693  dfnrm2  49677  dfnrm3  49678