Definition df-rab 3420

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 3083. (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 3419	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1569	. . . . 5 class 𝑥
6	5, 3	wcel 2146	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2744	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1570	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is used by:  rabbidva2  3421  cbvrabv  3429  rabeqcda  3430  rabrabi  3438  nfrab1  3439  rabid  3440  rabbida4  3444  rabbi  3449  rabid2f  3450  rabid2im  3451  cbvrabw  3454  nfrabw  3455  nfrab  3456  cbvrab  3457  rabab  3488  elrabi  3649  elrabf  3650  elrab3t  3652  elrab  3653  elrab2w  3658  ralrab2  3664  rexrab2  3666  cbvrabcsfw  3897  cbvrabcsf  3901  dfin5  3916  dfdif2  3917  ss2rab  4026  rabss  4027  ssrab  4028  ss2rabd  4029  rabss2  4034  rabss2OLD  4035  rabssab  4042  notab  4270  unrab  4271  inrab  4272  inrab2  4273  difrab  4274  dfrab3  4275  notrab  4278  rabun2  4280  dfnul3  4293  rab0OLD  4346  rabeq0w  4347  rabeq0  4348  dfif6  4495  rabeqsn  4638  rabsssn  4639  rabsnifsb  4693  reusn  4698  rabsneu  4700  elunirab  4892  elintrab  4930  ssintrab  4941  iunrab  5022  iinrab  5038  intexrab  5322  rmorabex  5446  exss  5449  rabxp  5714  mptpreima  6244  setlikespec  6333  predres  6347  fndmin  7047  fncnvima2  7063  riotauni  7386  riotacl2  7396  snriota  7413  orduniss2  7838  exse2  7923  zfrep6OLD  7961  xp2  8032  unielxp  8033  dfopab2  8058  suppvalbr  8169  ressuppss  8188  rankval3b  9808  scottabf  9878  scottexsOLD  9882  scott0bsOLD  9884  kardexOLD  9897  cardval2  9996  r0weon  10015  axdc2lem  10450  sstskm  10845  negfi  12182  nnzrab  12640  nn0zrab  12641  prprrab  14530  wrdnval  14602  shftlem  15131  shftuz  15132  shftdm  15134  hashbc0  17090  cshwsiun  17184  nfchnd  18692  submgmacs  18800  submacs  18911  eqglact  19272  cycsubg  19304  dfrhm2  20582  znunithash  21744  aspval2  22078  psrbaglefi  22106  clsval2  23237  xkoptsub  23841  ptcmplem2  24240  cnblcld  24961  cncmet  25511  shft2rab  25697  sca2rab  25701  vmappw  27310  2lgslem1b  27586  madeval2  28056  nb3grprlem1  29760  vtxdun  29861  rusgrprc  29970  ewlksfval  29981  wwlksnfi  30285  rusgrnumwwlkb0  30353  eclclwwlkn1  30456  clwwlkvbij  30494  h2hcau  31361  dfch2  31789  hhcno  32286  hhcnf  32287  pjhmopidm  32565  elpjrn  32572  dmrab  32873  rabsspr  32877  rabsstp  32878  rabfmpunirn  33028  mptctf  33091  maprnin  33106  fpwrelmapffslem  33107  fpwrelmap  33108  sigaex  34524  sigaval  34525  bnj1441  35252  bnj1441g  35253  bnj110  35270  fnrelpredd  35499  rabeqbii  36739  cbvrabdavw  36806  cbvrabdavw2  36830  neibastop3  36906  bj-rababw  37549  bj-inrab  37596  rabiun  38277  ptrest  38303  poimirlem26  38330  poimirlem27  38331  cnambfre  38352  areacirclem5  38396  ispridlc  38754  eqrabi  38938  ec1cnvres  38958  eccnvepres  38968  lkrval2  39897  lfl1dim  39928  glbconxN  40185  dva1dim  41792  dib1dim2  41975  diclspsn  42001  dih1dimatlem  42136  dihglb2  42149  hdmapoc  42738  sticksstones23  42969  aks6d1c6isolem3  42976  prjspeclsp  43377  eq0rabdioph  43540  rexrabdioph  43554  eldioph4b  43571  aomclem4  43817  onsucrn  44031  dfno2  44187  harval3  44297  alephiso2  44317  clcnvlem  44382  ntrneiel2  44845  rabexgf  45777  ssrabf  45865  rabssf  45870  cbvrabv2w  45879  rabbida2  45883  rabbida3  45886  f1oresf1o  48060  sprvalpw  48262  prprvalpw  48297  prprspr2  48300  stgr1  48759  dfnrm2  49743  dfnrm3  49744