Definition df-rab 3431

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 3059. (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 3430	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1532	. . . . 5 class 𝑥
6	5, 3	wcel 2098	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 394	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2705	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1533	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3432  rabbiiaOLD  3435  cbvrabv  3441  rabeqcda  3442  rabrabi  3449  nfrab1  3450  rabid  3451  rabrab  3454  rabbida4  3456  rabbi  3461  rabid2f  3462  rabid2OLD  3464  rabeqf  3465  cbvrabw  3466  nfrabw  3467  nfrabwOLD  3468  rabeqiOLD  3470  nfrab  3471  cbvrab  3472  rabab  3502  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  4068  rabss  4069  ssrab  4070  rabss2  4075  ssrab2OLD  4078  rabssab  4083  notab  4307  unrab  4308  inrab  4309  inrab2  4310  difrab  4311  dfrab3  4312  notrab  4315  rabun2  4317  dfnul3  4330  dfnul3OLD  4332  rab0  4386  rabeq0w  4387  rabeq0  4388  dfif6  4535  rabsneq  4650  rabeqsn  4674  rabsssn  4675  rabsnifsb  4731  reusn  4736  rabsneu  4738  elunirab  4927  elintrab  4967  ssintrab  4978  iunrab  5059  iinrab  5076  intexrab  5346  rmorabex  5466  exss  5469  rabxp  5730  mptpreima  6247  setlikespec  6336  predres  6350  fndmin  7059  fncnvima2  7075  riotauni  7388  riotacl2  7399  snriota  7416  orduniss2  7842  exse2  7931  zfrep6  7964  xp2  8036  unielxp  8037  dfopab2  8062  suppvalbr  8175  ressuppss  8194  rankval3b  9857  scottexs  9918  scott0s  9919  kardex  9925  cardval2  10022  r0weon  10043  axdc2lem  10479  sstskm  10873  negfi  12201  nnzrab  12628  nn0zrab  12629  prprrab  14474  wrdnval  14535  cshwsexaOLD  14815  shftlem  15055  shftuz  15056  shftdm  15058  hashbc0  16981  cshwsiun  17076  submgmacs  18684  submacs  18786  eqglact  19141  cycsubg  19170  dfrhm2  20420  znunithash  21505  aspval2  21838  psrbaglefi  21872  psrbaglefiOLD  21873  clsval2  22974  xkoptsub  23578  ptcmplem2  23977  cnblcld  24711  cncmet  25270  shft2rab  25457  sca2rab  25461  vmappw  27068  2lgslem1b  27345  madeval2  27800  nb3grprlem1  29213  vtxdun  29315  rusgrprc  29424  ewlksfval  29435  wwlksnfi  29737  rusgrnumwwlkb0  29802  eclclwwlkn1  29905  clwwlkvbij  29943  h2hcau  30809  dfch2  31237  hhcno  31734  hhcnf  31735  pjhmopidm  32013  elpjrn  32020  dmrab  32316  rabfmpunirn  32460  mptctf  32520  maprnin  32534  fpwrelmapffslem  32535  fpwrelmap  32536  sigaex  33762  sigaval  33763  bnj1441  34504  bnj1441g  34505  bnj110  34522  fnrelpredd  34745  neibastop3  35879  bj-rababw  36392  bj-inrab  36438  rabiun  37099  ptrest  37125  poimirlem26  37152  poimirlem27  37153  cnambfre  37174  areacirclem5  37218  ispridlc  37576  eccnvepres  37784  lkrval2  38594  lfl1dim  38625  glbconxN  38883  dva1dim  40490  dib1dim2  40673  diclspsn  40699  dih1dimatlem  40834  dihglb2  40847  hdmapoc  41436  sticksstones23  41673  aks6d1c6isolem3  41680  prjspeclsp  42067  elrab2w  42123  eq0rabdioph  42227  rexrabdioph  42245  eldioph4b  42262  aomclem4  42512  onsucrn  42731  dfno2  42889  harval3  42999  alephiso2  43019  clcnvlem  43084  ntrneiel2  43547  scottabf  43708  rabexgf  44417  ssrabf  44511  rabssf  44516  rabbida2  44529  rabbida3  44532  f1oresf1o  46699  sprvalpw  46849  prprvalpw  46884  prprspr2  46887  dfnrm2  48028  dfnrm3  48029