Definition df-rab 3391

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 3053. (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 3390	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1541	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2715	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1542	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3392  cbvrabv  3400  rabeqcda  3401  rabrabi  3409  nfrab1  3410  rabid  3411  rabbida4  3415  rabbi  3420  rabid2f  3421  rabid2im  3422  cbvrabw  3425  cbvrabwOLD  3426  nfrabw  3427  nfrab  3428  cbvrab  3429  rabab  3461  elrabi  3631  elrabf  3632  elrab3t  3634  elrab  3635  elrab2w  3639  ralrab2  3645  rexrab2  3647  cbvrabcsfw  3879  cbvrabcsf  3883  dfin5  3898  dfdif2  3899  ss2rab  4010  rabss  4011  ssrab  4012  ss2rabd  4013  rabss2  4018  rabss2OLD  4019  rabssab  4026  notab  4255  unrab  4256  inrab  4257  inrab2  4258  difrab  4259  dfrab3  4260  notrab  4263  rabun2  4265  dfnul3  4278  rab0  4327  rabeq0w  4328  rabeq0  4329  dfif6  4470  rabeqsn  4612  rabsssn  4613  rabsnifsb  4667  reusn  4672  rabsneu  4674  elunirab  4866  elintrab  4903  ssintrab  4914  iunrab  4996  iinrab  5012  intexrab  5289  rmorabex  5413  exss  5416  rabxp  5679  mptpreima  6203  setlikespec  6290  predres  6304  fndmin  6998  fncnvima2  7014  riotauni  7330  riotacl2  7340  snriota  7357  orduniss2  7784  exse2  7868  zfrep6OLD  7908  xp2  7979  unielxp  7980  dfopab2  8005  suppvalbr  8114  ressuppss  8133  rankval3b  9750  scottexs  9811  scott0s  9812  kardex  9818  cardval2  9915  r0weon  9934  axdc2lem  10370  sstskm  10765  negfi  12105  nnzrab  12555  nn0zrab  12556  prprrab  14435  wrdnval  14507  shftlem  15030  shftuz  15031  shftdm  15033  hashbc0  16976  cshwsiun  17070  nfchnd  18577  submgmacs  18685  submacs  18795  eqglact  19154  cycsubg  19183  dfrhm2  20454  znunithash  21544  aspval2  21878  psrbaglefi  21906  clsval2  23015  xkoptsub  23619  ptcmplem2  24018  cnblcld  24739  cncmet  25289  shft2rab  25475  sca2rab  25479  vmappw  27079  2lgslem1b  27355  madeval2  27825  nb3grprlem1  29449  vtxdun  29550  rusgrprc  29659  ewlksfval  29670  wwlksnfi  29974  rusgrnumwwlkb0  30042  eclclwwlkn1  30145  clwwlkvbij  30183  h2hcau  31050  dfch2  31478  hhcno  31975  hhcnf  31976  pjhmopidm  32254  elpjrn  32261  dmrab  32566  rabsspr  32571  rabsstp  32572  rabfmpunirn  32726  mptctf  32789  maprnin  32804  fpwrelmapffslem  32805  fpwrelmap  32806  sigaex  34254  sigaval  34255  bnj1441  34982  bnj1441g  34983  bnj110  35000  fnrelpredd  35234  rabeqbii  36376  cbvrabdavw  36443  cbvrabdavw2  36467  neibastop3  36544  bj-rababw  37188  bj-inrab  37234  rabiun  37914  ptrest  37940  poimirlem26  37967  poimirlem27  37968  cnambfre  37989  areacirclem5  38033  ispridlc  38391  eqrabi  38577  ec1cnvres  38597  eccnvepres  38607  lkrval2  39536  lfl1dim  39567  glbconxN  39824  dva1dim  41431  dib1dim2  41614  diclspsn  41640  dih1dimatlem  41775  dihglb2  41788  hdmapoc  42377  sticksstones23  42608  aks6d1c6isolem3  42615  prjspeclsp  43045  eq0rabdioph  43208  rexrabdioph  43222  eldioph4b  43239  aomclem4  43485  onsucrn  43699  dfno2  43855  harval3  43965  alephiso2  43985  clcnvlem  44050  ntrneiel2  44513  scottabf  44667  rabexgf  45455  ssrabf  45544  rabssf  45549  cbvrabv2w  45558  rabbida2  45562  rabbida3  45565  f1oresf1o  47732  sprvalpw  47934  prprvalpw  47969  prprspr2  47972  stgr1  48431  dfnrm2  49401  dfnrm3  49402