Definition df-rab 3433

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 3059. (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 3432	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1535	. . . . 5 class 𝑥
6	5, 3	wcel 2105	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2711	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1536	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3434  rabbiiaOLD  3437  cbvrabv  3443  rabeqcda  3444  rabrabi  3452  nfrab1  3453  rabid  3454  rabrab  3457  rabbida4  3459  rabbi  3464  rabid2f  3465  rabid2im  3466  rabid2OLD  3468  rabeqf  3469  cbvrabw  3470  cbvrabwOLD  3471  nfrabw  3472  nfrabwOLD  3473  nfrab  3475  cbvrab  3476  rabab  3509  elrabi  3689  elrabf  3690  rabeqcOLD  3692  elrab3t  3693  elrab  3694  elrab2w  3698  ralrab2  3706  rexrab2  3708  cbvrabcsfw  3951  cbvrabcsf  3955  dfin5  3970  dfdif2  3971  ss2rab  4080  rabss  4081  ssrab  4082  rabss2  4087  rabssab  4094  notab  4319  unrab  4320  inrab  4321  inrab2  4322  difrab  4323  dfrab3  4324  notrab  4327  rabun2  4329  dfnul3  4342  rab0  4391  rabeq0w  4392  rabeq0  4393  dfif6  4533  rabsneq  4648  rabeqsn  4671  rabsssn  4672  rabsnifsb  4726  reusn  4731  rabsneu  4733  elunirab  4926  elintrab  4964  ssintrab  4975  iunrab  5056  iinrab  5073  intexrab  5352  rmorabex  5470  exss  5473  rabxp  5736  mptpreima  6259  setlikespec  6347  predres  6361  fndmin  7064  fncnvima2  7080  riotauni  7393  riotacl2  7403  snriota  7420  orduniss2  7852  exse2  7939  zfrep6  7977  xp2  8049  unielxp  8050  dfopab2  8075  suppvalbr  8187  ressuppss  8206  rankval3b  9863  scottexs  9924  scott0s  9925  kardex  9931  cardval2  10028  r0weon  10049  axdc2lem  10485  sstskm  10879  negfi  12214  nnzrab  12642  nn0zrab  12643  prprrab  14508  wrdnval  14579  cshwsexaOLD  14859  shftlem  15103  shftuz  15104  shftdm  15106  hashbc0  17038  cshwsiun  17133  submgmacs  18742  submacs  18852  eqglact  19209  cycsubg  19238  dfrhm2  20490  znunithash  21600  aspval2  21935  psrbaglefi  21963  clsval2  23073  xkoptsub  23677  ptcmplem2  24076  cnblcld  24810  cncmet  25369  shft2rab  25556  sca2rab  25560  vmappw  27173  2lgslem1b  27450  madeval2  27906  nb3grprlem1  29411  vtxdun  29513  rusgrprc  29622  ewlksfval  29633  wwlksnfi  29935  rusgrnumwwlkb0  30000  eclclwwlkn1  30103  clwwlkvbij  30141  h2hcau  31007  dfch2  31435  hhcno  31932  hhcnf  31933  pjhmopidm  32211  elpjrn  32218  dmrab  32524  rabsspr  32528  rabsstp  32529  rabfmpunirn  32669  mptctf  32734  maprnin  32748  fpwrelmapffslem  32749  fpwrelmap  32750  sigaex  34090  sigaval  34091  bnj1441  34832  bnj1441g  34833  bnj110  34850  fnrelpredd  35081  rabeqbii  36175  cbvrabdavw  36243  cbvrabdavw2  36267  neibastop3  36344  bj-rababw  36863  bj-inrab  36909  rabiun  37579  ptrest  37605  poimirlem26  37632  poimirlem27  37633  cnambfre  37654  areacirclem5  37698  ispridlc  38056  eccnvepres  38261  lkrval2  39071  lfl1dim  39102  glbconxN  39360  dva1dim  40967  dib1dim2  41150  diclspsn  41176  dih1dimatlem  41311  dihglb2  41324  hdmapoc  41913  sticksstones23  42150  aks6d1c6isolem3  42157  prjspeclsp  42598  eq0rabdioph  42763  rexrabdioph  42781  eldioph4b  42798  aomclem4  43045  onsucrn  43260  dfno2  43417  harval3  43527  alephiso2  43547  clcnvlem  43612  ntrneiel2  44075  scottabf  44235  rabexgf  44961  ssrabf  45053  rabssf  45058  cbvrabv2w  45067  rabbida2  45071  rabbida3  45074  f1oresf1o  47239  sprvalpw  47404  prprvalpw  47439  prprspr2  47442  stgr1  47863  dfnrm2  48727  dfnrm3  48728