Definition df-rab 3393

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 3055. (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 3392	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1546	. . . . 5 class 𝑥
6	5, 3	wcel 2119	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 396	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2718	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1547	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3394  cbvrabv  3402  rabeqcda  3403  rabrabi  3411  nfrab1  3412  rabid  3413  rabbida4  3417  rabbi  3422  rabid2f  3423  rabid2im  3424  cbvrabw  3427  cbvrabwOLD  3428  nfrabw  3429  nfrab  3430  cbvrab  3431  rabab  3463  elrabi  3632  elrabf  3633  elrab3t  3635  elrab  3636  elrab2w  3640  ralrab2  3646  rexrab2  3648  cbvrabcsfw  3879  cbvrabcsf  3883  dfin5  3898  dfdif2  3899  ss2rab  4007  rabss  4008  ssrab  4009  ss2rabd  4010  rabss2  4015  rabss2OLD  4016  rabssab  4023  notab  4249  unrab  4250  inrab  4251  inrab2  4252  difrab  4253  dfrab3  4254  notrab  4257  rabun2  4259  dfnul3  4272  rab0  4321  rabeq0w  4322  rabeq0  4323  dfif6  4464  rabeqsn  4606  rabsssn  4607  rabsnifsb  4661  reusn  4666  rabsneu  4668  elunirab  4860  elintrab  4897  ssintrab  4908  iunrab  4989  iinrab  5005  intexrab  5282  rmorabex  5406  exss  5409  rabxp  5673  mptpreima  6196  setlikespec  6283  predres  6297  fndmin  6993  fncnvima2  7009  riotauni  7326  riotacl2  7336  snriota  7353  orduniss2  7780  exse2  7864  zfrep6OLD  7904  xp2  7975  unielxp  7976  dfopab2  8001  suppvalbr  8111  ressuppss  8130  rankval3b  9748  scottexs  9809  scott0s  9810  kardex  9816  cardval2  9913  r0weon  9932  axdc2lem  10368  sstskm  10763  negfi  12103  nnzrab  12553  nn0zrab  12554  prprrab  14433  wrdnval  14505  shftlem  15028  shftuz  15029  shftdm  15031  hashbc0  16974  cshwsiun  17068  nfchnd  18575  submgmacs  18683  submacs  18793  eqglact  19152  cycsubg  19181  dfrhm2  20452  znunithash  21546  aspval2  21880  psrbaglefi  21908  clsval2  23040  xkoptsub  23644  ptcmplem2  24043  cnblcld  24764  cncmet  25314  shft2rab  25500  sca2rab  25504  vmappw  27104  2lgslem1b  27380  madeval2  27850  nb3grprlem1  29474  vtxdun  29575  rusgrprc  29684  ewlksfval  29695  wwlksnfi  29999  rusgrnumwwlkb0  30067  eclclwwlkn1  30170  clwwlkvbij  30208  h2hcau  31075  dfch2  31503  hhcno  32000  hhcnf  32001  pjhmopidm  32279  elpjrn  32286  dmrab  32591  rabsspr  32596  rabsstp  32597  rabfmpunirn  32752  mptctf  32815  maprnin  32830  fpwrelmapffslem  32831  fpwrelmap  32832  sigaex  34301  sigaval  34302  bnj1441  35029  bnj1441g  35030  bnj110  35047  fnrelpredd  35281  rabeqbii  36423  cbvrabdavw  36490  cbvrabdavw2  36514  neibastop3  36591  bj-rababw  37235  bj-inrab  37281  rabiun  37961  ptrest  37987  poimirlem26  38014  poimirlem27  38015  cnambfre  38036  areacirclem5  38080  ispridlc  38438  eqrabi  38624  ec1cnvres  38644  eccnvepres  38654  lkrval2  39583  lfl1dim  39614  glbconxN  39871  dva1dim  41478  dib1dim2  41661  diclspsn  41687  dih1dimatlem  41822  dihglb2  41835  hdmapoc  42424  sticksstones23  42655  aks6d1c6isolem3  42662  prjspeclsp  43063  eq0rabdioph  43226  rexrabdioph  43240  eldioph4b  43257  aomclem4  43503  onsucrn  43717  dfno2  43873  harval3  43983  alephiso2  44003  clcnvlem  44068  ntrneiel2  44531  scottabf  44685  rabexgf  45473  ssrabf  45562  rabssf  45567  cbvrabv2w  45576  rabbida2  45580  rabbida3  45583  f1oresf1o  47754  sprvalpw  47956  prprvalpw  47991  prprspr2  47994  stgr1  48453  dfnrm2  49423  dfnrm3  49424