Definition df-rab 3414

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 3076. (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 3413	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1558	. . . . 5 class 𝑥
6	5, 3	wcel 2141	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2739	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1559	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3415  cbvrabv  3423  rabeqcda  3424  rabrabi  3432  nfrab1  3433  rabid  3434  rabbida4  3438  rabbi  3443  rabid2f  3444  rabid2im  3445  cbvrabw  3448  cbvrabwOLD  3449  nfrabw  3450  nfrab  3451  cbvrab  3452  rabab  3483  elrabi  3646  elrabf  3647  elrab3t  3649  elrab  3650  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  4339  rabeq0w  4340  rabeq0  4341  dfif6  4482  rabeqsn  4625  rabsssn  4626  rabsnifsb  4680  reusn  4685  rabsneu  4687  elunirab  4879  elintrab  4917  ssintrab  4928  iunrab  5009  iinrab  5025  intexrab  5302  rmorabex  5426  exss  5429  rabxp  5693  mptpreima  6219  setlikespec  6306  predres  6320  fndmin  7020  fncnvima2  7036  riotauni  7353  riotacl2  7363  snriota  7380  orduniss2  7807  exse2  7892  zfrep6OLD  7930  xp2  8001  unielxp  8002  dfopab2  8027  suppvalbr  8137  ressuppss  8156  rankval3b  9779  scottexs  9840  scott0s  9841  kardex  9847  cardval2  9944  r0weon  9963  axdc2lem  10400  sstskm  10795  negfi  12136  nnzrab  12594  nn0zrab  12595  prprrab  14481  wrdnval  14553  shftlem  15076  shftuz  15077  shftdm  15079  hashbc0  17022  cshwsiun  17116  nfchnd  18624  submgmacs  18732  submacs  18842  eqglact  19201  cycsubg  19230  dfrhm2  20500  znunithash  21594  aspval2  21928  psrbaglefi  21956  clsval2  23088  xkoptsub  23692  ptcmplem2  24091  cnblcld  24812  cncmet  25362  shft2rab  25548  sca2rab  25552  vmappw  27155  2lgslem1b  27431  madeval2  27901  nb3grprlem1  29525  vtxdun  29626  rusgrprc  29735  ewlksfval  29746  wwlksnfi  30050  rusgrnumwwlkb0  30118  eclclwwlkn1  30221  clwwlkvbij  30259  h2hcau  31126  dfch2  31554  hhcno  32051  hhcnf  32052  pjhmopidm  32330  elpjrn  32337  dmrab  32642  rabsspr  32647  rabsstp  32648  rabfmpunirn  32803  mptctf  32866  maprnin  32881  fpwrelmapffslem  32882  fpwrelmap  32883  sigaex  34366  sigaval  34367  bnj1441  35097  bnj1441g  35098  bnj110  35115  fnrelpredd  35347  rabeqbii  36507  cbvrabdavw  36574  cbvrabdavw2  36598  neibastop3  36675  bj-rababw  37319  bj-inrab  37365  rabiun  38045  ptrest  38071  poimirlem26  38098  poimirlem27  38099  cnambfre  38120  areacirclem5  38164  ispridlc  38522  eqrabi  38708  ec1cnvres  38728  eccnvepres  38738  lkrval2  39667  lfl1dim  39698  glbconxN  39955  dva1dim  41562  dib1dim2  41745  diclspsn  41771  dih1dimatlem  41906  dihglb2  41919  hdmapoc  42508  sticksstones23  42739  aks6d1c6isolem3  42746  prjspeclsp  43147  eq0rabdioph  43310  rexrabdioph  43324  eldioph4b  43341  aomclem4  43587  onsucrn  43801  dfno2  43957  harval3  44067  alephiso2  44087  clcnvlem  44152  ntrneiel2  44615  scottabf  44769  rabexgf  45557  ssrabf  45645  rabssf  45650  cbvrabv2w  45659  rabbida2  45663  rabbida3  45666  f1oresf1o  47837  sprvalpw  48039  prprvalpw  48074  prprspr2  48077  stgr1  48536  dfnrm2  49506  dfnrm3  49507