Definition df-rab 3434

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 3063. (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 3433	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1541	. . . . 5 class 𝑥
6	5, 3	wcel 2107	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 397	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2710	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1542	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3435  rabbiiaOLD  3438  cbvrabv  3443  rabeqcda  3444  rabrabi  3451  nfrab1  3452  rabid  3453  rabrab  3456  rabbida4  3458  rabbi  3463  rabid2f  3464  rabid2OLD  3466  rabeqf  3467  cbvrabw  3468  nfrabw  3469  nfrabwOLD  3470  rabeqiOLD  3472  nfrab  3473  cbvrab  3474  rabab  3503  elrabi  3678  elrabiOLD  3679  elrabf  3680  rabeqcOLD  3682  elrab3t  3683  elrab  3684  ralrab2  3695  rexrab2  3697  cbvrabcsfw  3938  cbvrabcsf  3942  dfin5  3957  dfdif2  3958  ss2rab  4069  rabss  4070  ssrab  4071  rabss2  4076  ssrab2OLD  4079  rabssab  4084  notab  4305  unrab  4306  inrab  4307  inrab2  4308  difrab  4309  dfrab3  4310  notrab  4312  rabun2  4314  dfnul3  4327  dfnul3OLD  4329  rab0  4383  rabeq0w  4384  rabeq0  4385  dfif6  4532  rabeqsn  4670  rabsssn  4671  rabsnifsb  4727  reusn  4732  rabsneu  4734  elunirab  4925  elintrab  4965  ssintrab  4976  iunrab  5056  iinrab  5073  intexrab  5341  rmorabex  5461  exss  5464  rabxp  5725  mptpreima  6238  setlikespec  6327  predres  6341  fndmin  7047  fncnvima2  7063  riotauni  7371  riotacl2  7382  snriota  7399  orduniss2  7821  exse2  7908  zfrep6  7941  xp2  8012  unielxp  8013  dfopab2  8038  suppvalbr  8150  ressuppss  8168  rankval3b  9821  scottexs  9882  scott0s  9883  kardex  9889  cardval2  9986  r0weon  10007  axdc2lem  10443  sstskm  10837  negfi  12163  nnzrab  12590  nn0zrab  12591  prprrab  14434  wrdnval  14495  cshwsexaOLD  14775  shftlem  15015  shftuz  15016  shftdm  15018  hashbc0  16938  cshwsiun  17033  submacs  18708  eqglact  19059  cycsubg  19085  dfrhm2  20253  znunithash  21120  aspval2  21452  psrbaglefi  21485  psrbaglefiOLD  21486  clsval2  22554  xkoptsub  23158  ptcmplem2  23557  cnblcld  24291  cncmet  24839  shft2rab  25025  sca2rab  25029  vmappw  26620  2lgslem1b  26895  madeval2  27348  nb3grprlem1  28637  vtxdun  28738  rusgrprc  28847  ewlksfval  28858  wwlksnfi  29160  rusgrnumwwlkb0  29225  eclclwwlkn1  29328  clwwlkvbij  29366  h2hcau  30232  dfch2  30660  hhcno  31157  hhcnf  31158  pjhmopidm  31436  elpjrn  31443  dmrab  31737  rabfmpunirn  31878  mptctf  31942  maprnin  31956  fpwrelmapffslem  31957  fpwrelmap  31958  sigaex  33108  sigaval  33109  bnj1441  33851  bnj1441g  33852  bnj110  33869  fnrelpredd  34092  neibastop3  35247  bj-rababw  35761  bj-inrab  35807  rabiun  36461  ptrest  36487  poimirlem26  36514  poimirlem27  36515  cnambfre  36536  areacirclem5  36580  ispridlc  36938  eccnvepres  37148  lkrval2  37960  lfl1dim  37991  glbconxN  38249  dva1dim  39856  dib1dim2  40039  diclspsn  40065  dih1dimatlem  40200  dihglb2  40213  hdmapoc  40802  prjspeclsp  41354  elrab2w  41410  eq0rabdioph  41514  rexrabdioph  41532  eldioph4b  41549  aomclem4  41799  onsucrn  42021  dfno2  42179  harval3  42289  alephiso2  42309  clcnvlem  42374  ntrneiel2  42837  scottabf  42999  rabexgf  43708  ssrabf  43803  rabssf  43808  rabbida2  43821  rabbida3  43824  f1oresf1o  45998  sprvalpw  46148  prprvalpw  46183  prprspr2  46186  submgmacs  46574  dfnrm2  47564  dfnrm3  47565