Definition df-rab 3409

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 3046. (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 3408	. 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 2708	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1540	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3410  rabbiiaOLD  3413  cbvrabv  3419  rabeqcda  3420  rabrabi  3428  nfrab1  3429  rabid  3430  rabrab  3433  rabbida4  3434  rabbi  3439  rabid2f  3440  rabid2im  3441  rabeqf  3443  cbvrabw  3444  cbvrabwOLD  3445  nfrabw  3446  nfrab  3448  cbvrab  3449  rabab  3481  elrabi  3657  elrabf  3658  rabeqcOLD  3660  elrab3t  3661  elrab  3662  elrab2w  3666  ralrab2  3672  rexrab2  3674  cbvrabcsfw  3906  cbvrabcsf  3910  dfin5  3925  dfdif2  3926  ss2rab  4037  rabss  4038  ssrab  4039  rabss2  4044  rabssab  4051  notab  4280  unrab  4281  inrab  4282  inrab2  4283  difrab  4284  dfrab3  4285  notrab  4288  rabun2  4290  dfnul3  4303  rab0  4352  rabeq0w  4353  rabeq0  4354  dfif6  4494  rabsneq  4611  rabeqsn  4634  rabsssn  4635  rabsnifsb  4689  reusn  4694  rabsneu  4696  elunirab  4889  elintrab  4927  ssintrab  4938  iunrab  5019  iinrab  5036  intexrab  5305  rmorabex  5423  exss  5426  rabxp  5689  mptpreima  6214  setlikespec  6301  predres  6315  fndmin  7020  fncnvima2  7036  riotauni  7353  riotacl2  7363  snriota  7380  orduniss2  7811  exse2  7896  zfrep6  7936  xp2  8008  unielxp  8009  dfopab2  8034  suppvalbr  8146  ressuppss  8165  rankval3b  9786  scottexs  9847  scott0s  9848  kardex  9854  cardval2  9951  r0weon  9972  axdc2lem  10408  sstskm  10802  negfi  12139  nnzrab  12568  nn0zrab  12569  prprrab  14445  wrdnval  14517  cshwsexaOLD  14797  shftlem  15041  shftuz  15042  shftdm  15044  hashbc0  16983  cshwsiun  17077  submgmacs  18651  submacs  18761  eqglact  19118  cycsubg  19147  dfrhm2  20390  znunithash  21481  aspval2  21814  psrbaglefi  21842  clsval2  22944  xkoptsub  23548  ptcmplem2  23947  cnblcld  24669  cncmet  25229  shft2rab  25416  sca2rab  25420  vmappw  27033  2lgslem1b  27310  madeval2  27768  nb3grprlem1  29314  vtxdun  29416  rusgrprc  29525  ewlksfval  29536  wwlksnfi  29843  rusgrnumwwlkb0  29908  eclclwwlkn1  30011  clwwlkvbij  30049  h2hcau  30915  dfch2  31343  hhcno  31840  hhcnf  31841  pjhmopidm  32119  elpjrn  32126  dmrab  32433  rabsspr  32437  rabsstp  32438  rabfmpunirn  32584  mptctf  32648  maprnin  32661  fpwrelmapffslem  32662  fpwrelmap  32663  sigaex  34107  sigaval  34108  bnj1441  34837  bnj1441g  34838  bnj110  34855  fnrelpredd  35086  rabeqbii  36189  cbvrabdavw  36256  cbvrabdavw2  36280  neibastop3  36357  bj-rababw  36876  bj-inrab  36922  rabiun  37594  ptrest  37620  poimirlem26  37647  poimirlem27  37648  cnambfre  37669  areacirclem5  37713  ispridlc  38071  eccnvepres  38275  lkrval2  39090  lfl1dim  39121  glbconxN  39379  dva1dim  40986  dib1dim2  41169  diclspsn  41195  dih1dimatlem  41330  dihglb2  41343  hdmapoc  41932  sticksstones23  42164  aks6d1c6isolem3  42171  prjspeclsp  42607  eq0rabdioph  42771  rexrabdioph  42789  eldioph4b  42806  aomclem4  43053  onsucrn  43267  dfno2  43424  harval3  43534  alephiso2  43554  clcnvlem  43619  ntrneiel2  44082  scottabf  44236  rabexgf  45025  ssrabf  45115  rabssf  45120  cbvrabv2w  45129  rabbida2  45133  rabbida3  45136  f1oresf1o  47295  sprvalpw  47485  prprvalpw  47520  prprspr2  47523  stgr1  47964  dfnrm2  48924  dfnrm3  48925