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  27349  nb3grprlem1  28668  vtxdun  28769  rusgrprc  28878  ewlksfval  28889  wwlksnfi  29191  rusgrnumwwlkb0  29256  eclclwwlkn1  29359  clwwlkvbij  29397  h2hcau  30263  dfch2  30691  hhcno  31188  hhcnf  31189  pjhmopidm  31467  elpjrn  31474  dmrab  31768  rabfmpunirn  31909  mptctf  31973  maprnin  31987  fpwrelmapffslem  31988  fpwrelmap  31989  sigaex  33139  sigaval  33140  bnj1441  33882  bnj1441g  33883  bnj110  33900  fnrelpredd  34123  neibastop3  35295  bj-rababw  35809  bj-inrab  35855  rabiun  36509  ptrest  36535  poimirlem26  36562  poimirlem27  36563  cnambfre  36584  areacirclem5  36628  ispridlc  36986  eccnvepres  37196  lkrval2  38008  lfl1dim  38039  glbconxN  38297  dva1dim  39904  dib1dim2  40087  diclspsn  40113  dih1dimatlem  40248  dihglb2  40261  hdmapoc  40850  prjspeclsp  41402  elrab2w  41458  eq0rabdioph  41562  rexrabdioph  41580  eldioph4b  41597  aomclem4  41847  onsucrn  42069  dfno2  42227  harval3  42337  alephiso2  42357  clcnvlem  42422  ntrneiel2  42885  scottabf  43047  rabexgf  43756  ssrabf  43851  rabssf  43856  rabbida2  43869  rabbida3  43872  f1oresf1o  46046  sprvalpw  46196  prprvalpw  46231  prprspr2  46234  submgmacs  46622  dfnrm2  47612  dfnrm3  47613