Definition df-rab 3444

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 3068. (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 3443	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1536	. . . . 5 class 𝑥
6	5, 3	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2717	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1537	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3445  rabbiiaOLD  3448  cbvrabv  3454  rabeqcda  3455  rabrabi  3463  nfrab1  3464  rabid  3465  rabrab  3468  rabbida4  3470  rabbi  3475  rabid2f  3476  rabid2im  3477  rabid2OLD  3479  rabeqf  3480  cbvrabw  3481  cbvrabwOLD  3482  nfrabw  3483  nfrabwOLD  3484  nfrab  3486  cbvrab  3487  rabab  3520  elrabi  3703  elrabf  3704  rabeqcOLD  3706  elrab3t  3707  elrab  3708  elrab2w  3712  ralrab2  3720  rexrab2  3722  cbvrabcsfw  3965  cbvrabcsf  3969  dfin5  3984  dfdif2  3985  ss2rab  4094  rabss  4095  ssrab  4096  rabss2  4101  rabssab  4108  notab  4333  unrab  4334  inrab  4335  inrab2  4336  difrab  4337  dfrab3  4338  notrab  4341  rabun2  4343  dfnul3  4356  dfnul3OLD  4358  rab0  4409  rabeq0w  4410  rabeq0  4411  dfif6  4551  rabsneq  4666  rabeqsn  4689  rabsssn  4690  rabsnifsb  4747  reusn  4752  rabsneu  4754  elunirab  4946  elintrab  4984  ssintrab  4995  iunrab  5075  iinrab  5092  intexrab  5365  rmorabex  5480  exss  5483  rabxp  5748  mptpreima  6269  setlikespec  6357  predres  6371  fndmin  7078  fncnvima2  7094  riotauni  7410  riotacl2  7421  snriota  7438  orduniss2  7869  exse2  7957  zfrep6  7995  xp2  8067  unielxp  8068  dfopab2  8093  suppvalbr  8205  ressuppss  8224  rankval3b  9895  scottexs  9956  scott0s  9957  kardex  9963  cardval2  10060  r0weon  10081  axdc2lem  10517  sstskm  10911  negfi  12244  nnzrab  12671  nn0zrab  12672  prprrab  14522  wrdnval  14593  cshwsexaOLD  14873  shftlem  15117  shftuz  15118  shftdm  15120  hashbc0  17052  cshwsiun  17147  submgmacs  18755  submacs  18862  eqglact  19219  cycsubg  19248  dfrhm2  20500  znunithash  21606  aspval2  21941  psrbaglefi  21969  clsval2  23079  xkoptsub  23683  ptcmplem2  24082  cnblcld  24816  cncmet  25375  shft2rab  25562  sca2rab  25566  vmappw  27177  2lgslem1b  27454  madeval2  27910  nb3grprlem1  29415  vtxdun  29517  rusgrprc  29626  ewlksfval  29637  wwlksnfi  29939  rusgrnumwwlkb0  30004  eclclwwlkn1  30107  clwwlkvbij  30145  h2hcau  31011  dfch2  31439  hhcno  31936  hhcnf  31937  pjhmopidm  32215  elpjrn  32222  dmrab  32525  rabsspr  32529  rabsstp  32530  rabfmpunirn  32671  mptctf  32731  maprnin  32745  fpwrelmapffslem  32746  fpwrelmap  32747  sigaex  34074  sigaval  34075  bnj1441  34816  bnj1441g  34817  bnj110  34834  fnrelpredd  35065  rabeqbii  36158  cbvrabdavw  36227  cbvrabdavw2  36251  neibastop3  36328  bj-rababw  36847  bj-inrab  36893  rabiun  37553  ptrest  37579  poimirlem26  37606  poimirlem27  37607  cnambfre  37628  areacirclem5  37672  ispridlc  38030  eccnvepres  38236  lkrval2  39046  lfl1dim  39077  glbconxN  39335  dva1dim  40942  dib1dim2  41125  diclspsn  41151  dih1dimatlem  41286  dihglb2  41299  hdmapoc  41888  sticksstones23  42126  aks6d1c6isolem3  42133  prjspeclsp  42567  eq0rabdioph  42732  rexrabdioph  42750  eldioph4b  42767  aomclem4  43014  onsucrn  43233  dfno2  43390  harval3  43500  alephiso2  43520  clcnvlem  43585  ntrneiel2  44048  scottabf  44209  rabexgf  44924  ssrabf  45016  rabssf  45021  cbvrabv2w  45030  rabbida2  45034  rabbida3  45037  f1oresf1o  47205  sprvalpw  47354  prprvalpw  47389  prprspr2  47392  dfnrm2  48611  dfnrm3  48612