Definition df-rab 3421

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 3051. (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 3420	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1538	. . . . 5 class 𝑥
6	5, 3	wcel 2107	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2712	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1539	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3422  rabbiiaOLD  3425  cbvrabv  3431  rabeqcda  3432  rabrabi  3440  nfrab1  3441  rabid  3442  rabrab  3445  rabbida4  3446  rabbi  3451  rabid2f  3452  rabid2im  3453  rabid2OLD  3455  rabeqf  3456  cbvrabw  3457  cbvrabwOLD  3458  nfrabw  3459  nfrabwOLD  3460  nfrab  3462  cbvrab  3463  rabab  3496  elrabi  3671  elrabf  3672  rabeqcOLD  3674  elrab3t  3675  elrab  3676  elrab2w  3680  ralrab2  3688  rexrab2  3690  cbvrabcsfw  3922  cbvrabcsf  3926  dfin5  3941  dfdif2  3942  ss2rab  4053  rabss  4054  ssrab  4055  rabss2  4060  rabssab  4067  notab  4296  unrab  4297  inrab  4298  inrab2  4299  difrab  4300  dfrab3  4301  notrab  4304  rabun2  4306  dfnul3  4319  rab0  4368  rabeq0w  4369  rabeq0  4370  dfif6  4510  rabsneq  4626  rabeqsn  4649  rabsssn  4650  rabsnifsb  4704  reusn  4709  rabsneu  4711  elunirab  4904  elintrab  4942  ssintrab  4953  iunrab  5034  iinrab  5051  intexrab  5329  rmorabex  5447  exss  5450  rabxp  5715  mptpreima  6240  setlikespec  6327  predres  6341  fndmin  7046  fncnvima2  7062  riotauni  7377  riotacl2  7387  snriota  7404  orduniss2  7836  exse2  7922  zfrep6  7962  xp2  8034  unielxp  8035  dfopab2  8060  suppvalbr  8172  ressuppss  8191  rankval3b  9849  scottexs  9910  scott0s  9911  kardex  9917  cardval2  10014  r0weon  10035  axdc2lem  10471  sstskm  10865  negfi  12200  nnzrab  12629  nn0zrab  12630  prprrab  14495  wrdnval  14566  cshwsexaOLD  14846  shftlem  15090  shftuz  15091  shftdm  15093  hashbc0  17026  cshwsiun  17120  submgmacs  18700  submacs  18810  eqglact  19167  cycsubg  19196  dfrhm2  20443  znunithash  21546  aspval2  21881  psrbaglefi  21909  clsval2  23019  xkoptsub  23623  ptcmplem2  24022  cnblcld  24746  cncmet  25307  shft2rab  25494  sca2rab  25498  vmappw  27110  2lgslem1b  27387  madeval2  27843  nb3grprlem1  29340  vtxdun  29442  rusgrprc  29551  ewlksfval  29562  wwlksnfi  29869  rusgrnumwwlkb0  29934  eclclwwlkn1  30037  clwwlkvbij  30075  h2hcau  30941  dfch2  31369  hhcno  31866  hhcnf  31867  pjhmopidm  32145  elpjrn  32152  dmrab  32459  rabsspr  32463  rabsstp  32464  rabfmpunirn  32606  mptctf  32672  maprnin  32685  fpwrelmapffslem  32686  fpwrelmap  32687  sigaex  34048  sigaval  34049  bnj1441  34791  bnj1441g  34792  bnj110  34809  fnrelpredd  35040  rabeqbii  36132  cbvrabdavw  36199  cbvrabdavw2  36223  neibastop3  36300  bj-rababw  36819  bj-inrab  36865  rabiun  37537  ptrest  37563  poimirlem26  37590  poimirlem27  37591  cnambfre  37612  areacirclem5  37656  ispridlc  38014  eccnvepres  38218  lkrval2  39028  lfl1dim  39059  glbconxN  39317  dva1dim  40924  dib1dim2  41107  diclspsn  41133  dih1dimatlem  41268  dihglb2  41281  hdmapoc  41870  sticksstones23  42107  aks6d1c6isolem3  42114  prjspeclsp  42563  eq0rabdioph  42728  rexrabdioph  42746  eldioph4b  42763  aomclem4  43010  onsucrn  43225  dfno2  43382  harval3  43492  alephiso2  43512  clcnvlem  43577  ntrneiel2  44040  scottabf  44200  rabexgf  44970  ssrabf  45060  rabssf  45065  cbvrabv2w  45074  rabbida2  45078  rabbida3  45081  f1oresf1o  47244  sprvalpw  47409  prprvalpw  47444  prprspr2  47447  stgr1  47870  dfnrm2  48773  dfnrm3  48774