Definition df-rab 3401

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 3400	. 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  3402  cbvrabv  3410  rabeqcda  3411  rabrabi  3419  nfrab1  3420  rabid  3421  rabrab  3424  rabbida4  3425  rabbi  3430  rabid2f  3431  rabid2im  3432  rabeqf  3434  cbvrabw  3435  cbvrabwOLD  3436  nfrabw  3437  nfrab  3439  cbvrab  3440  rabab  3472  elrabi  3643  elrabf  3644  elrab3t  3646  elrab  3647  elrab2w  3651  ralrab2  3657  rexrab2  3659  cbvrabcsfw  3891  cbvrabcsf  3895  dfin5  3910  dfdif2  3911  ss2rab  4022  rabss  4023  ssrab  4024  ss2rabd  4025  rabss2  4030  rabss2OLD  4031  rabssab  4038  notab  4267  unrab  4268  inrab  4269  inrab2  4270  difrab  4271  dfrab3  4272  notrab  4275  rabun2  4277  dfnul3  4290  rab0  4339  rabeq0w  4340  rabeq0  4341  dfif6  4483  rabsneq  4600  rabeqsn  4625  rabsssn  4626  rabsnifsb  4680  reusn  4685  rabsneu  4687  elunirab  4879  elintrab  4916  ssintrab  4927  iunrab  5009  iinrab  5025  intexrab  5293  rmorabex  5409  exss  5412  rabxp  5673  mptpreima  6197  setlikespec  6284  predres  6298  fndmin  6992  fncnvima2  7008  riotauni  7323  riotacl2  7333  snriota  7350  orduniss2  7777  exse2  7861  zfrep6  7901  xp2  7972  unielxp  7973  dfopab2  7998  suppvalbr  8108  ressuppss  8127  rankval3b  9742  scottexs  9803  scott0s  9804  kardex  9810  cardval2  9907  r0weon  9926  axdc2lem  10362  sstskm  10757  negfi  12095  nnzrab  12523  nn0zrab  12524  prprrab  14400  wrdnval  14472  shftlem  14995  shftuz  14996  shftdm  14998  hashbc0  16937  cshwsiun  17031  nfchnd  18538  submgmacs  18646  submacs  18756  eqglact  19112  cycsubg  19141  dfrhm2  20414  znunithash  21523  aspval2  21858  psrbaglefi  21886  clsval2  22998  xkoptsub  23602  ptcmplem2  24001  cnblcld  24722  cncmet  25282  shft2rab  25469  sca2rab  25473  vmappw  27086  2lgslem1b  27363  madeval2  27831  nb3grprlem1  29436  vtxdun  29538  rusgrprc  29647  ewlksfval  29658  wwlksnfi  29962  rusgrnumwwlkb0  30030  eclclwwlkn1  30133  clwwlkvbij  30171  h2hcau  31037  dfch2  31465  hhcno  31962  hhcnf  31963  pjhmopidm  32241  elpjrn  32248  dmrab  32553  rabsspr  32558  rabsstp  32559  rabfmpunirn  32713  mptctf  32776  maprnin  32791  fpwrelmapffslem  32792  fpwrelmap  32793  sigaex  34248  sigaval  34249  bnj1441  34977  bnj1441g  34978  bnj110  34995  fnrelpredd  35228  rabeqbii  36369  cbvrabdavw  36436  cbvrabdavw2  36460  neibastop3  36537  bj-rababw  37057  bj-inrab  37103  rabiun  37765  ptrest  37791  poimirlem26  37818  poimirlem27  37819  cnambfre  37840  areacirclem5  37884  ispridlc  38242  eqrabi  38429  ec1cnvres  38448  eccnvepres  38458  lkrval2  39387  lfl1dim  39418  glbconxN  39675  dva1dim  41282  dib1dim2  41465  diclspsn  41491  dih1dimatlem  41626  dihglb2  41639  hdmapoc  42228  sticksstones23  42460  aks6d1c6isolem3  42467  prjspeclsp  42891  eq0rabdioph  43054  rexrabdioph  43072  eldioph4b  43089  aomclem4  43335  onsucrn  43549  dfno2  43705  harval3  43815  alephiso2  43835  clcnvlem  43900  ntrneiel2  44363  scottabf  44517  rabexgf  45305  ssrabf  45394  rabssf  45399  cbvrabv2w  45408  rabbida2  45412  rabbida3  45415  f1oresf1o  47572  sprvalpw  47762  prprvalpw  47797  prprspr2  47800  stgr1  48243  dfnrm2  49213  dfnrm3  49214