Definition df-rab 3398

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 3050. (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 3397	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2113	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2711	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1541	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3399  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  3640  elrabf  3641  elrab3t  3643  elrab  3644  elrab2w  3648  ralrab2  3654  rexrab2  3656  cbvrabcsfw  3888  cbvrabcsf  3892  dfin5  3907  dfdif2  3908  ss2rab  4019  rabss  4020  ssrab  4021  ss2rabd  4022  rabss2  4028  rabss2OLD  4029  rabssab  4036  notab  4265  unrab  4266  inrab  4267  inrab2  4268  difrab  4269  dfrab3  4270  notrab  4273  rabun2  4275  dfnul3  4288  rab0  4337  rabeq0w  4338  rabeq0  4339  dfif6  4479  rabsneq  4596  rabeqsn  4621  rabsssn  4622  rabsnifsb  4676  reusn  4681  rabsneu  4683  elunirab  4875  elintrab  4912  ssintrab  4923  iunrab  5005  iinrab  5021  intexrab  5289  rmorabex  5405  exss  5408  rabxp  5669  mptpreima  6193  setlikespec  6280  predres  6294  fndmin  6987  fncnvima2  7003  riotauni  7318  riotacl2  7328  snriota  7345  orduniss2  7772  exse2  7856  zfrep6  7896  xp2  7967  unielxp  7968  dfopab2  7993  suppvalbr  8103  ressuppss  8122  rankval3b  9729  scottexs  9790  scott0s  9791  kardex  9797  cardval2  9894  r0weon  9913  axdc2lem  10349  sstskm  10743  negfi  12081  nnzrab  12510  nn0zrab  12511  prprrab  14390  wrdnval  14462  shftlem  14985  shftuz  14986  shftdm  14988  hashbc0  16927  cshwsiun  17021  nfchnd  18527  submgmacs  18635  submacs  18745  eqglact  19101  cycsubg  19130  dfrhm2  20402  znunithash  21511  aspval2  21845  psrbaglefi  21873  clsval2  22975  xkoptsub  23579  ptcmplem2  23978  cnblcld  24699  cncmet  25259  shft2rab  25446  sca2rab  25450  vmappw  27063  2lgslem1b  27340  madeval2  27804  nb3grprlem1  29369  vtxdun  29471  rusgrprc  29580  ewlksfval  29591  wwlksnfi  29895  rusgrnumwwlkb0  29963  eclclwwlkn1  30066  clwwlkvbij  30104  h2hcau  30970  dfch2  31398  hhcno  31895  hhcnf  31896  pjhmopidm  32174  elpjrn  32181  dmrab  32487  rabsspr  32492  rabsstp  32493  rabfmpunirn  32646  mptctf  32710  maprnin  32725  fpwrelmapffslem  32726  fpwrelmap  32727  sigaex  34134  sigaval  34135  bnj1441  34863  bnj1441g  34864  bnj110  34881  fnrelpredd  35113  rabeqbii  36249  cbvrabdavw  36316  cbvrabdavw2  36340  neibastop3  36417  bj-rababw  36936  bj-inrab  36982  rabiun  37643  ptrest  37669  poimirlem26  37696  poimirlem27  37697  cnambfre  37718  areacirclem5  37762  ispridlc  38120  ec1cnvres  38318  eccnvepres  38328  lkrval2  39199  lfl1dim  39230  glbconxN  39487  dva1dim  41094  dib1dim2  41277  diclspsn  41303  dih1dimatlem  41438  dihglb2  41451  hdmapoc  42040  sticksstones23  42272  aks6d1c6isolem3  42279  prjspeclsp  42720  eq0rabdioph  42883  rexrabdioph  42901  eldioph4b  42918  aomclem4  43164  onsucrn  43378  dfno2  43535  harval3  43645  alephiso2  43665  clcnvlem  43730  ntrneiel2  44193  scottabf  44347  rabexgf  45135  ssrabf  45225  rabssf  45230  cbvrabv2w  45239  rabbida2  45243  rabbida3  45246  f1oresf1o  47404  sprvalpw  47594  prprvalpw  47629  prprspr2  47632  stgr1  48075  dfnrm2  49046  dfnrm3  49047