Definition df-rab 3391

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 3390	. 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  3392  cbvrabv  3400  rabeqcda  3401  rabrabi  3409  nfrab1  3410  rabid  3411  rabrab  3414  rabbida4  3415  rabbi  3420  rabid2f  3421  rabid2im  3422  rabeqf  3424  cbvrabw  3425  cbvrabwOLD  3426  nfrabw  3427  nfrab  3428  cbvrab  3429  rabab  3461  elrabi  3631  elrabf  3632  elrab3t  3634  elrab  3635  elrab2w  3639  ralrab2  3645  rexrab2  3647  cbvrabcsfw  3879  cbvrabcsf  3883  dfin5  3898  dfdif2  3899  ss2rab  4010  rabss  4011  ssrab  4012  ss2rabd  4013  rabss2  4018  rabss2OLD  4019  rabssab  4026  notab  4255  unrab  4256  inrab  4257  inrab2  4258  difrab  4259  dfrab3  4260  notrab  4263  rabun2  4265  dfnul3  4278  rab0  4327  rabeq0w  4328  rabeq0  4329  dfif6  4470  rabsneq  4587  rabeqsn  4612  rabsssn  4613  rabsnifsb  4667  reusn  4672  rabsneu  4674  elunirab  4866  elintrab  4903  ssintrab  4914  iunrab  4996  iinrab  5012  intexrab  5282  rmorabex  5405  exss  5408  rabxp  5670  mptpreima  6194  setlikespec  6281  predres  6295  fndmin  6989  fncnvima2  7005  riotauni  7321  riotacl2  7331  snriota  7348  orduniss2  7775  exse2  7859  zfrep6OLD  7899  xp2  7970  unielxp  7971  dfopab2  7996  suppvalbr  8105  ressuppss  8124  rankval3b  9739  scottexs  9800  scott0s  9801  kardex  9807  cardval2  9904  r0weon  9923  axdc2lem  10359  sstskm  10754  negfi  12094  nnzrab  12544  nn0zrab  12545  prprrab  14424  wrdnval  14496  shftlem  15019  shftuz  15020  shftdm  15022  hashbc0  16965  cshwsiun  17059  nfchnd  18566  submgmacs  18674  submacs  18784  eqglact  19143  cycsubg  19172  dfrhm2  20443  znunithash  21552  aspval2  21886  psrbaglefi  21914  clsval2  23024  xkoptsub  23628  ptcmplem2  24027  cnblcld  24748  cncmet  25298  shft2rab  25484  sca2rab  25488  vmappw  27097  2lgslem1b  27374  madeval2  27844  nb3grprlem1  29468  vtxdun  29570  rusgrprc  29679  ewlksfval  29690  wwlksnfi  29994  rusgrnumwwlkb0  30062  eclclwwlkn1  30165  clwwlkvbij  30203  h2hcau  31070  dfch2  31498  hhcno  31995  hhcnf  31996  pjhmopidm  32274  elpjrn  32281  dmrab  32586  rabsspr  32591  rabsstp  32592  rabfmpunirn  32746  mptctf  32809  maprnin  32824  fpwrelmapffslem  32825  fpwrelmap  32826  sigaex  34275  sigaval  34276  bnj1441  35003  bnj1441g  35004  bnj110  35021  fnrelpredd  35255  rabeqbii  36397  cbvrabdavw  36464  cbvrabdavw2  36488  neibastop3  36565  bj-rababw  37201  bj-inrab  37247  rabiun  37925  ptrest  37951  poimirlem26  37978  poimirlem27  37979  cnambfre  38000  areacirclem5  38044  ispridlc  38402  eqrabi  38588  ec1cnvres  38608  eccnvepres  38618  lkrval2  39547  lfl1dim  39578  glbconxN  39835  dva1dim  41442  dib1dim2  41625  diclspsn  41651  dih1dimatlem  41786  dihglb2  41799  hdmapoc  42388  sticksstones23  42619  aks6d1c6isolem3  42626  prjspeclsp  43056  eq0rabdioph  43219  rexrabdioph  43237  eldioph4b  43254  aomclem4  43500  onsucrn  43714  dfno2  43870  harval3  43980  alephiso2  44000  clcnvlem  44065  ntrneiel2  44528  scottabf  44682  rabexgf  45470  ssrabf  45559  rabssf  45564  cbvrabv2w  45573  rabbida2  45577  rabbida3  45580  f1oresf1o  47735  sprvalpw  47937  prprvalpw  47972  prprspr2  47975  stgr1  48434  dfnrm2  49404  dfnrm3  49405