Definition df-rab 3060

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 3056. (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 3055	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1542	. . . . 5 class 𝑥
6	5, 3	wcel 2112	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2714	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1543	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  3280  rabrab  3281  rabid2  3283  rabid2f  3284  rabbi  3285  nfrab1  3286  nfrabw  3287  nfrab  3288  rabbiia  3372  rabbidva2  3376  rabeqf  3381  rabeqiOLD  3383  cbvrabw  3390  cbvrab  3391  cbvrabv  3392  rabrabi  3393  rabeqcda  3395  rabab  3426  elrabi  3585  elrabiOLD  3586  elrabf  3587  rabeqc  3589  elrab3t  3590  elrab  3591  ralrab2  3601  rexrab2  3604  cbvrabcsfw  3842  cbvrabcsf  3846  dfin5  3861  dfdif2  3862  ss2rab  3970  rabss  3971  ssrab  3972  rabss2  3977  ssrab2OLD  3980  rabssab  3984  notab  4205  unrab  4206  inrab  4207  inrab2  4208  difrab  4209  dfrab3  4210  notrab  4212  rabun2  4214  dfnul3  4227  dfnul3OLD  4229  rab0  4283  rabeq0w  4284  rabeq0  4285  dfif6  4428  rabeqsn  4568  rabsssn  4569  rabsnifsb  4624  reusn  4629  rabsneu  4631  elunirab  4821  elintrab  4857  ssintrab  4868  iunrab  4947  iinrab  4963  intexrab  5218  rmorabex  5329  exss  5332  rabxp  5582  mptpreima  6081  setlikespec  6161  fndmin  6843  fncnvima2  6859  riotauni  7154  riotacl2  7165  snriota  7182  orduniss2  7590  exse2  7673  zfrep6  7706  xp2  7776  unielxp  7777  dfopab2  7800  suppvalbr  7885  ressuppss  7903  rankval3b  9407  scottexs  9468  scott0s  9469  kardex  9475  cardval2  9572  r0weon  9591  axdc2lem  10027  sstskm  10421  negfi  11746  nnzrab  12170  nn0zrab  12171  prprrab  14004  wrdnval  14065  cshwsexa  14354  shftlem  14596  shftuz  14597  shftdm  14599  hashbc0  16521  cshwsiun  16616  submacs  18207  eqglact  18549  cycsubg  18569  dfrhm2  19691  znunithash  20483  aspval2  20812  psrbaglefi  20845  psrbaglefiOLD  20846  clsval2  21901  xkoptsub  22505  ptcmplem2  22904  cnblcld  23626  cncmet  24173  shft2rab  24359  sca2rab  24363  vmappw  25952  2lgslem1b  26227  nb3grprlem1  27422  vtxdun  27523  rusgrprc  27632  ewlksfval  27643  wwlksnfi  27944  rusgrnumwwlkb0  28009  eclclwwlkn1  28112  clwwlkvbij  28150  h2hcau  29014  dfch2  29442  hhcno  29939  hhcnf  29940  pjhmopidm  30218  elpjrn  30225  dmrab  30517  rabfmpunirn  30664  mptctf  30726  maprnin  30740  fpwrelmapffslem  30741  fpwrelmap  30742  sigaex  31744  sigaval  31745  bnj1441  32487  bnj1441g  32488  bnj110  32505  fnrelpredd  32728  madeval2  33723  neibastop3  34237  bj-rababw  34753  bj-rabbida2  34793  bj-inrab  34801  rabiun  35436  ptrest  35462  poimirlem26  35489  poimirlem27  35490  cnambfre  35511  areacirclem5  35555  ispridlc  35914  eccnvepres  36101  lkrval2  36790  lfl1dim  36821  glbconxN  37078  dva1dim  38685  dib1dim2  38868  diclspsn  38894  dih1dimatlem  39029  dihglb2  39042  hdmapoc  39631  elrab2w  39830  prjspeclsp  40100  eq0rabdioph  40242  rexrabdioph  40260  eldioph4b  40277  aomclem4  40526  harval3  40769  alephiso2  40782  clcnvlem  40848  ntrneiel2  41314  scottabf  41472  rabexgf  42181  ssrabf  42278  rabssf  42282  rabbida2  42295  rabbida3  42298  f1oresf1o  44397  sprvalpw  44548  prprvalpw  44583  prprspr2  44586  submgmacs  44974  dfnrm2  45841  dfnrm3  45842