Definition df-rab 3406

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 3045. (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 3405	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2109	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2707	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1540	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3407  rabbiiaOLD  3410  cbvrabv  3416  rabeqcda  3417  rabrabi  3425  nfrab1  3426  rabid  3427  rabrab  3430  rabbida4  3431  rabbi  3436  rabid2f  3437  rabid2im  3438  rabeqf  3440  cbvrabw  3441  cbvrabwOLD  3442  nfrabw  3443  nfrab  3445  cbvrab  3446  rabab  3478  elrabi  3654  elrabf  3655  rabeqcOLD  3657  elrab3t  3658  elrab  3659  elrab2w  3663  ralrab2  3669  rexrab2  3671  cbvrabcsfw  3903  cbvrabcsf  3907  dfin5  3922  dfdif2  3923  ss2rab  4034  rabss  4035  ssrab  4036  rabss2  4041  rabssab  4048  notab  4277  unrab  4278  inrab  4279  inrab2  4280  difrab  4281  dfrab3  4282  notrab  4285  rabun2  4287  dfnul3  4300  rab0  4349  rabeq0w  4350  rabeq0  4351  dfif6  4491  rabsneq  4608  rabeqsn  4631  rabsssn  4632  rabsnifsb  4686  reusn  4691  rabsneu  4693  elunirab  4886  elintrab  4924  ssintrab  4935  iunrab  5016  iinrab  5033  intexrab  5302  rmorabex  5420  exss  5423  rabxp  5686  mptpreima  6211  setlikespec  6298  predres  6312  fndmin  7017  fncnvima2  7033  riotauni  7350  riotacl2  7360  snriota  7377  orduniss2  7808  exse2  7893  zfrep6  7933  xp2  8005  unielxp  8006  dfopab2  8031  suppvalbr  8143  ressuppss  8162  rankval3b  9779  scottexs  9840  scott0s  9841  kardex  9847  cardval2  9944  r0weon  9965  axdc2lem  10401  sstskm  10795  negfi  12132  nnzrab  12561  nn0zrab  12562  prprrab  14438  wrdnval  14510  cshwsexaOLD  14790  shftlem  15034  shftuz  15035  shftdm  15037  hashbc0  16976  cshwsiun  17070  submgmacs  18644  submacs  18754  eqglact  19111  cycsubg  19140  dfrhm2  20383  znunithash  21474  aspval2  21807  psrbaglefi  21835  clsval2  22937  xkoptsub  23541  ptcmplem2  23940  cnblcld  24662  cncmet  25222  shft2rab  25409  sca2rab  25413  vmappw  27026  2lgslem1b  27303  madeval2  27761  nb3grprlem1  29307  vtxdun  29409  rusgrprc  29518  ewlksfval  29529  wwlksnfi  29836  rusgrnumwwlkb0  29901  eclclwwlkn1  30004  clwwlkvbij  30042  h2hcau  30908  dfch2  31336  hhcno  31833  hhcnf  31834  pjhmopidm  32112  elpjrn  32119  dmrab  32426  rabsspr  32430  rabsstp  32431  rabfmpunirn  32577  mptctf  32641  maprnin  32654  fpwrelmapffslem  32655  fpwrelmap  32656  sigaex  34100  sigaval  34101  bnj1441  34830  bnj1441g  34831  bnj110  34848  fnrelpredd  35079  rabeqbii  36182  cbvrabdavw  36249  cbvrabdavw2  36273  neibastop3  36350  bj-rababw  36869  bj-inrab  36915  rabiun  37587  ptrest  37613  poimirlem26  37640  poimirlem27  37641  cnambfre  37662  areacirclem5  37706  ispridlc  38064  eccnvepres  38268  lkrval2  39083  lfl1dim  39114  glbconxN  39372  dva1dim  40979  dib1dim2  41162  diclspsn  41188  dih1dimatlem  41323  dihglb2  41336  hdmapoc  41925  sticksstones23  42157  aks6d1c6isolem3  42164  prjspeclsp  42600  eq0rabdioph  42764  rexrabdioph  42782  eldioph4b  42799  aomclem4  43046  onsucrn  43260  dfno2  43417  harval3  43527  alephiso2  43547  clcnvlem  43612  ntrneiel2  44075  scottabf  44229  rabexgf  45018  ssrabf  45108  rabssf  45113  cbvrabv2w  45122  rabbida2  45126  rabbida3  45129  f1oresf1o  47291  sprvalpw  47481  prprvalpw  47516  prprspr2  47519  stgr1  47960  dfnrm2  48920  dfnrm3  48921