Definition df-rab 3412

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 3047. (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 3411	. 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  3413  rabbiiaOLD  3416  cbvrabv  3422  rabeqcda  3423  rabrabi  3431  nfrab1  3432  rabid  3433  rabrab  3436  rabbida4  3437  rabbi  3442  rabid2f  3443  rabid2im  3444  rabid2OLD  3446  rabeqf  3447  cbvrabw  3448  cbvrabwOLD  3449  nfrabw  3450  nfrabwOLD  3451  nfrab  3453  cbvrab  3454  rabab  3487  elrabi  3662  elrabf  3663  rabeqcOLD  3665  elrab3t  3666  elrab  3667  elrab2w  3671  ralrab2  3677  rexrab2  3679  cbvrabcsfw  3911  cbvrabcsf  3915  dfin5  3930  dfdif2  3931  ss2rab  4042  rabss  4043  ssrab  4044  rabss2  4049  rabssab  4056  notab  4285  unrab  4286  inrab  4287  inrab2  4288  difrab  4289  dfrab3  4290  notrab  4293  rabun2  4295  dfnul3  4308  rab0  4357  rabeq0w  4358  rabeq0  4359  dfif6  4499  rabsneq  4616  rabeqsn  4639  rabsssn  4640  rabsnifsb  4694  reusn  4699  rabsneu  4701  elunirab  4894  elintrab  4932  ssintrab  4943  iunrab  5024  iinrab  5041  intexrab  5310  rmorabex  5428  exss  5431  rabxp  5694  mptpreima  6219  setlikespec  6306  predres  6320  fndmin  7024  fncnvima2  7040  riotauni  7357  riotacl2  7367  snriota  7384  orduniss2  7816  exse2  7902  zfrep6  7942  xp2  8014  unielxp  8015  dfopab2  8040  suppvalbr  8152  ressuppss  8171  rankval3b  9797  scottexs  9858  scott0s  9859  kardex  9865  cardval2  9962  r0weon  9983  axdc2lem  10419  sstskm  10813  negfi  12148  nnzrab  12577  nn0zrab  12578  prprrab  14448  wrdnval  14520  cshwsexaOLD  14800  shftlem  15044  shftuz  15045  shftdm  15047  hashbc0  16982  cshwsiun  17076  submgmacs  18650  submacs  18760  eqglact  19117  cycsubg  19146  dfrhm2  20389  znunithash  21480  aspval2  21813  psrbaglefi  21841  clsval2  22943  xkoptsub  23547  ptcmplem2  23946  cnblcld  24668  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  32585  mptctf  32649  maprnin  32662  fpwrelmapffslem  32663  fpwrelmap  32664  sigaex  34108  sigaval  34109  bnj1441  34838  bnj1441g  34839  bnj110  34856  fnrelpredd  35087  rabeqbii  36179  cbvrabdavw  36246  cbvrabdavw2  36270  neibastop3  36347  bj-rababw  36866  bj-inrab  36912  rabiun  37584  ptrest  37610  poimirlem26  37637  poimirlem27  37638  cnambfre  37659  areacirclem5  37703  ispridlc  38061  eccnvepres  38265  lkrval2  39075  lfl1dim  39106  glbconxN  39364  dva1dim  40971  dib1dim2  41154  diclspsn  41180  dih1dimatlem  41315  dihglb2  41328  hdmapoc  41917  sticksstones23  42149  aks6d1c6isolem3  42156  prjspeclsp  42572  eq0rabdioph  42736  rexrabdioph  42754  eldioph4b  42771  aomclem4  43018  onsucrn  43232  dfno2  43389  harval3  43499  alephiso2  43519  clcnvlem  43584  ntrneiel2  44047  scottabf  44201  rabexgf  44990  ssrabf  45080  rabssf  45085  cbvrabv2w  45094  rabbida2  45098  rabbida3  45101  f1oresf1o  47261  sprvalpw  47436  prprvalpw  47471  prprspr2  47474  stgr1  47915  dfnrm2  48848  dfnrm3  48849