Definition df-rab 3402

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 3053. (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 3401	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1541	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2715	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1542	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3403  cbvrabv  3411  rabeqcda  3412  rabrabi  3420  nfrab1  3421  rabid  3422  rabrab  3425  rabbida4  3426  rabbi  3431  rabid2f  3432  rabid2im  3433  rabeqf  3435  cbvrabw  3436  cbvrabwOLD  3437  nfrabw  3438  nfrab  3440  cbvrab  3441  rabab  3473  elrabi  3644  elrabf  3645  elrab3t  3647  elrab  3648  elrab2w  3652  ralrab2  3658  rexrab2  3660  cbvrabcsfw  3892  cbvrabcsf  3896  dfin5  3911  dfdif2  3912  ss2rab  4023  rabss  4024  ssrab  4025  ss2rabd  4026  rabss2  4031  rabss2OLD  4032  rabssab  4039  notab  4268  unrab  4269  inrab  4270  inrab2  4271  difrab  4272  dfrab3  4273  notrab  4276  rabun2  4278  dfnul3  4291  rab0  4340  rabeq0w  4341  rabeq0  4342  dfif6  4484  rabsneq  4601  rabeqsn  4626  rabsssn  4627  rabsnifsb  4681  reusn  4686  rabsneu  4688  elunirab  4880  elintrab  4917  ssintrab  4928  iunrab  5010  iinrab  5026  intexrab  5294  rmorabex  5415  exss  5418  rabxp  5680  mptpreima  6204  setlikespec  6291  predres  6305  fndmin  6999  fncnvima2  7015  riotauni  7331  riotacl2  7341  snriota  7358  orduniss2  7785  exse2  7869  zfrep6  7909  xp2  7980  unielxp  7981  dfopab2  8006  suppvalbr  8116  ressuppss  8135  rankval3b  9750  scottexs  9811  scott0s  9812  kardex  9818  cardval2  9915  r0weon  9934  axdc2lem  10370  sstskm  10765  negfi  12103  nnzrab  12531  nn0zrab  12532  prprrab  14408  wrdnval  14480  shftlem  15003  shftuz  15004  shftdm  15006  hashbc0  16945  cshwsiun  17039  nfchnd  18546  submgmacs  18654  submacs  18764  eqglact  19120  cycsubg  19149  dfrhm2  20422  znunithash  21531  aspval2  21866  psrbaglefi  21894  clsval2  23006  xkoptsub  23610  ptcmplem2  24009  cnblcld  24730  cncmet  25290  shft2rab  25477  sca2rab  25481  vmappw  27094  2lgslem1b  27371  madeval2  27841  nb3grprlem1  29465  vtxdun  29567  rusgrprc  29676  ewlksfval  29687  wwlksnfi  29991  rusgrnumwwlkb0  30059  eclclwwlkn1  30162  clwwlkvbij  30200  h2hcau  31066  dfch2  31494  hhcno  31991  hhcnf  31992  pjhmopidm  32270  elpjrn  32277  dmrab  32582  rabsspr  32587  rabsstp  32588  rabfmpunirn  32742  mptctf  32805  maprnin  32820  fpwrelmapffslem  32821  fpwrelmap  32822  sigaex  34287  sigaval  34288  bnj1441  35015  bnj1441g  35016  bnj110  35033  fnrelpredd  35266  rabeqbii  36407  cbvrabdavw  36474  cbvrabdavw2  36498  neibastop3  36575  bj-rababw  37120  bj-inrab  37166  rabiun  37833  ptrest  37859  poimirlem26  37886  poimirlem27  37887  cnambfre  37908  areacirclem5  37952  ispridlc  38310  eqrabi  38496  ec1cnvres  38516  eccnvepres  38526  lkrval2  39455  lfl1dim  39486  glbconxN  39743  dva1dim  41350  dib1dim2  41533  diclspsn  41559  dih1dimatlem  41694  dihglb2  41707  hdmapoc  42296  sticksstones23  42528  aks6d1c6isolem3  42535  prjspeclsp  42959  eq0rabdioph  43122  rexrabdioph  43140  eldioph4b  43157  aomclem4  43403  onsucrn  43617  dfno2  43773  harval3  43883  alephiso2  43903  clcnvlem  43968  ntrneiel2  44431  scottabf  44585  rabexgf  45373  ssrabf  45462  rabssf  45467  cbvrabv2w  45476  rabbida2  45480  rabbida3  45483  f1oresf1o  47639  sprvalpw  47829  prprvalpw  47864  prprspr2  47867  stgr1  48310  dfnrm2  49280  dfnrm3  49281