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 3051. (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 1538	. . . . 5 class 𝑥
6	5, 3	wcel 2107	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2712	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1539	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3421  rabbiiaOLD  3424  cbvrabv  3430  rabeqcda  3431  rabrabi  3439  nfrab1  3440  rabid  3441  rabrab  3444  rabbida4  3445  rabbi  3450  rabid2f  3451  rabid2im  3452  rabid2OLD  3454  rabeqf  3455  cbvrabw  3456  cbvrabwOLD  3457  nfrabw  3458  nfrabwOLD  3459  nfrab  3461  cbvrab  3462  rabab  3495  elrabi  3670  elrabf  3671  rabeqcOLD  3673  elrab3t  3674  elrab  3675  elrab2w  3679  ralrab2  3686  rexrab2  3688  cbvrabcsfw  3920  cbvrabcsf  3924  dfin5  3939  dfdif2  3940  ss2rab  4051  rabss  4052  ssrab  4053  rabss2  4058  rabssab  4065  notab  4294  unrab  4295  inrab  4296  inrab2  4297  difrab  4298  dfrab3  4299  notrab  4302  rabun2  4304  dfnul3  4317  rab0  4366  rabeq0w  4367  rabeq0  4368  dfif6  4508  rabsneq  4624  rabeqsn  4647  rabsssn  4648  rabsnifsb  4702  reusn  4707  rabsneu  4709  elunirab  4902  elintrab  4940  ssintrab  4951  iunrab  5032  iinrab  5049  intexrab  5327  rmorabex  5445  exss  5448  rabxp  5713  mptpreima  6238  setlikespec  6325  predres  6339  fndmin  7045  fncnvima2  7061  riotauni  7376  riotacl2  7386  snriota  7403  orduniss2  7835  exse2  7921  zfrep6  7961  xp2  8033  unielxp  8034  dfopab2  8059  suppvalbr  8171  ressuppss  8190  rankval3b  9848  scottexs  9909  scott0s  9910  kardex  9916  cardval2  10013  r0weon  10034  axdc2lem  10470  sstskm  10864  negfi  12199  nnzrab  12628  nn0zrab  12629  prprrab  14495  wrdnval  14566  cshwsexaOLD  14846  shftlem  15090  shftuz  15091  shftdm  15093  hashbc0  17026  cshwsiun  17120  submgmacs  18700  submacs  18810  eqglact  19167  cycsubg  19196  dfrhm2  20443  znunithash  21538  aspval2  21873  psrbaglefi  21901  clsval2  23005  xkoptsub  23609  ptcmplem2  24008  cnblcld  24732  cncmet  25293  shft2rab  25480  sca2rab  25484  vmappw  27096  2lgslem1b  27373  madeval2  27829  nb3grprlem1  29326  vtxdun  29428  rusgrprc  29537  ewlksfval  29548  wwlksnfi  29855  rusgrnumwwlkb0  29920  eclclwwlkn1  30023  clwwlkvbij  30061  h2hcau  30927  dfch2  31355  hhcno  31852  hhcnf  31853  pjhmopidm  32131  elpjrn  32138  dmrab  32445  rabsspr  32449  rabsstp  32450  rabfmpunirn  32599  mptctf  32665  maprnin  32678  fpwrelmapffslem  32679  fpwrelmap  32680  sigaex  34086  sigaval  34087  bnj1441  34829  bnj1441g  34830  bnj110  34847  fnrelpredd  35078  rabeqbii  36170  cbvrabdavw  36237  cbvrabdavw2  36261  neibastop3  36338  bj-rababw  36857  bj-inrab  36903  rabiun  37575  ptrest  37601  poimirlem26  37628  poimirlem27  37629  cnambfre  37650  areacirclem5  37694  ispridlc  38052  eccnvepres  38256  lkrval2  39066  lfl1dim  39097  glbconxN  39355  dva1dim  40962  dib1dim2  41145  diclspsn  41171  dih1dimatlem  41306  dihglb2  41319  hdmapoc  41908  sticksstones23  42145  aks6d1c6isolem3  42152  prjspeclsp  42601  eq0rabdioph  42765  rexrabdioph  42783  eldioph4b  42800  aomclem4  43047  onsucrn  43261  dfno2  43418  harval3  43528  alephiso2  43548  clcnvlem  43613  ntrneiel2  44076  scottabf  44231  rabexgf  45001  ssrabf  45091  rabssf  45096  cbvrabv2w  45105  rabbida2  45109  rabbida3  45112  f1oresf1o  47275  sprvalpw  47440  prprvalpw  47475  prprspr2  47478  stgr1  47901  dfnrm2  48813  dfnrm3  48814