Definition df-rab 3397

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

This definition is referenced by:  rabbidva2  3398  rabbiiaOLD  3401  cbvrabv  3407  rabeqcda  3408  rabrabi  3416  nfrab1  3417  rabid  3418  rabrab  3421  rabbida4  3422  rabbi  3427  rabid2f  3428  rabid2im  3429  rabeqf  3431  cbvrabw  3432  cbvrabwOLD  3433  nfrabw  3434  nfrab  3436  cbvrab  3437  rabab  3469  elrabi  3645  elrabf  3646  rabeqcOLD  3648  elrab3t  3649  elrab  3650  elrab2w  3654  ralrab2  3660  rexrab2  3662  cbvrabcsfw  3894  cbvrabcsf  3898  dfin5  3913  dfdif2  3914  ss2rab  4024  rabss  4025  ssrab  4026  rabss2  4031  rabssab  4038  notab  4267  unrab  4268  inrab  4269  inrab2  4270  difrab  4271  dfrab3  4272  notrab  4275  rabun2  4277  dfnul3  4290  rab0  4339  rabeq0w  4340  rabeq0  4341  dfif6  4481  rabsneq  4598  rabeqsn  4621  rabsssn  4622  rabsnifsb  4676  reusn  4681  rabsneu  4683  elunirab  4876  elintrab  4913  ssintrab  4924  iunrab  5004  iinrab  5021  intexrab  5289  rmorabex  5407  exss  5410  rabxp  5671  mptpreima  6191  setlikespec  6277  predres  6291  fndmin  6983  fncnvima2  6999  riotauni  7316  riotacl2  7326  snriota  7343  orduniss2  7772  exse2  7857  zfrep6  7897  xp2  7968  unielxp  7969  dfopab2  7994  suppvalbr  8104  ressuppss  8123  rankval3b  9741  scottexs  9802  scott0s  9803  kardex  9809  cardval2  9906  r0weon  9925  axdc2lem  10361  sstskm  10755  negfi  12092  nnzrab  12521  nn0zrab  12522  prprrab  14398  wrdnval  14470  cshwsexaOLD  14749  shftlem  14993  shftuz  14994  shftdm  14996  hashbc0  16935  cshwsiun  17029  submgmacs  18609  submacs  18719  eqglact  19076  cycsubg  19105  dfrhm2  20377  znunithash  21489  aspval2  21823  psrbaglefi  21851  clsval2  22953  xkoptsub  23557  ptcmplem2  23956  cnblcld  24678  cncmet  25238  shft2rab  25425  sca2rab  25429  vmappw  27042  2lgslem1b  27319  madeval2  27781  nb3grprlem1  29343  vtxdun  29445  rusgrprc  29554  ewlksfval  29565  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  32610  mptctf  32674  maprnin  32687  fpwrelmapffslem  32688  fpwrelmap  32689  sigaex  34076  sigaval  34077  bnj1441  34806  bnj1441g  34807  bnj110  34824  fnrelpredd  35055  rabeqbii  36167  cbvrabdavw  36234  cbvrabdavw2  36258  neibastop3  36335  bj-rababw  36854  bj-inrab  36900  rabiun  37572  ptrest  37598  poimirlem26  37625  poimirlem27  37626  cnambfre  37647  areacirclem5  37691  ispridlc  38049  eccnvepres  38253  lkrval2  39068  lfl1dim  39099  glbconxN  39357  dva1dim  40964  dib1dim2  41147  diclspsn  41173  dih1dimatlem  41308  dihglb2  41321  hdmapoc  41910  sticksstones23  42142  aks6d1c6isolem3  42149  prjspeclsp  42585  eq0rabdioph  42749  rexrabdioph  42767  eldioph4b  42784  aomclem4  43030  onsucrn  43244  dfno2  43401  harval3  43511  alephiso2  43531  clcnvlem  43596  ntrneiel2  44059  scottabf  44213  rabexgf  45002  ssrabf  45092  rabssf  45097  cbvrabv2w  45106  rabbida2  45110  rabbida3  45113  f1oresf1o  47275  sprvalpw  47465  prprvalpw  47500  prprspr2  47503  stgr1  47944  dfnrm2  48904  dfnrm3  48905