Definition df-rab 3414

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

This definition is used by:  rabbidva2  3415  cbvrabv  3423  rabeqcda  3424  rabrabi  3431  nfrab1  3432  rabid  3433  rabbida4  3437  rabbi  3442  rabid2f  3443  rabid2im  3444  cbvrabw  3447  nfrabw  3448  nfrab  3449  cbvrab  3450  rabab  3481  elrabi  3641  elrabf  3642  elrab3t  3644  elrab  3645  elrab2w  3650  ralrab2  3656  rexrab2  3658  cbvrabcsfw  3888  cbvrabcsf  3892  dfin5  3907  dfdif2  3908  ss2rab  4017  rabss  4018  ssrab  4019  ss2rabd  4020  rabss2  4025  rabss2OLD  4026  rabssab  4033  notab  4260  unrab  4261  inrab  4262  inrab2  4263  difrab  4264  dfrab3  4265  notrab  4268  rabun2  4270  dfnul3  4283  rab0OLD  4336  rabeq0w  4337  rabeq0  4338  dfif6  4485  rabeqsn  4628  rabsssn  4629  rabsnifsb  4683  reusn  4688  rabsneu  4690  elunirab  4882  elintrab  4920  ssintrab  4931  iunrab  5011  iinrab  5027  intexrab  5308  rmorabex  5428  exss  5431  rabxp  5699  mptpreima  6232  setlikespec  6321  predres  6335  fndmin  7036  fncnvima2  7052  riotauni  7375  riotacl2  7385  snriota  7402  orduniss2  7833  exse2  7918  zfrep6OLD  7956  xp2  8027  unielxp  8028  dfopab2  8052  suppvalbr  8165  ressuppss  8184  rankval3b  9815  scottabf  9917  scottexsOLD  9921  scott0bsOLD  9923  kardexOLD  9936  cardval2  10050  r0weon  10069  axdc2lem  10504  sstskm  10905  negfi  12244  nnzrab  12702  nn0zrab  12703  prprrab  14595  wrdnval  14667  shftlem  15198  shftuz  15199  shftdm  15201  hashbc0  17160  cshwsiun  17254  nfchnd  18762  submgmacs  18883  submacs  19000  eqglact  19368  cycsubg  19400  dfrhm2  20681  znunithash  21847  aspval2  22183  psrbaglefi  22211  clsval2  23345  xkoptsub  23950  ptcmplem2  24349  cnblcld  25070  cncmet  25620  shft2rab  25806  sca2rab  25810  vmappw  27422  2lgslem1b  27698  madeval2  28198  nb3grprlem1  29940  vtxdun  30041  rusgrprc  30150  ewlksfval  30161  wwlksnfi  30474  rusgrnumwwlkb0  30542  eclclwwlkn1  30645  clwwlkvbij  30683  h2hcau  31560  dfch2  31988  hhcno  32485  hhcnf  32486  pjhmopidm  32764  elpjrn  32771  dmrab  33072  rabsspr  33076  rabsstp  33077  rabfmpunirn  33226  mptctf  33287  maprnin  33302  fpwrelmapffslem  33303  fpwrelmap  33304  sigaex  34721  sigaval  34722  bnj1441  35450  bnj1441g  35451  bnj110  35468  fnrelpredd  35696  rabeqbii  36950  cbvrabdavw  37017  cbvrabdavw2  37041  neibastop3  37117  bj-rababw  37760  bj-inrab  37807  rabiun  38486  ptrest  38502  poimirlem26  38529  poimirlem27  38530  cnambfre  38551  areacirclem5  38595  ispridlc  38969  eqrabi  39153  ec1cnvres  39173  eccnvepres  39183  lkrval2  40112  lfl1dim  40143  glbconxN  40400  dva1dim  42007  dib1dim2  42190  diclspsn  42216  dih1dimatlem  42351  dihglb2  42364  hdmapoc  42953  sticksstones23  43184  aks6d1c6isolem3  43191  prjspeclsp  43599  eq0rabdioph  43737  rexrabdioph  43751  eldioph4b  43768  aomclem4  44014  onsucrn  44228  dfno2  44384  harval3  44494  alephiso2  44514  clcnvlem  44579  ntrneiel2  45042  rabexgf  45981  ssrabf  46069  rabssf  46074  cbvrabv2w  46083  rabbida2  46087  rabbida3  46090  f1oresf1o  48301  sprvalpw  48503  prprvalpw  48538  prprspr2  48541  stgr1  49000  dfnrm2  49981  dfnrm3  49982