Definition df-rab 3072

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

This definition is referenced by:  rabid  3304  rabrab  3305  rabid2  3307  rabid2f  3308  rabbi  3309  nfrab1  3310  nfrabw  3311  nfrab  3312  rabbiia  3396  rabbidva2  3400  rabeqf  3405  rabeqiOLD  3407  cbvrabw  3414  cbvrab  3415  cbvrabv  3416  rabrabi  3417  rabeqcda  3419  rabab  3450  elrabi  3611  elrabiOLD  3612  elrabf  3613  rabeqc  3615  elrab3t  3616  elrab  3617  ralrab2  3629  rexrab2  3632  cbvrabcsfw  3872  cbvrabcsf  3876  dfin5  3891  dfdif2  3892  ss2rab  4000  rabss  4001  ssrab  4002  rabss2  4007  ssrab2OLD  4010  rabssab  4014  notab  4235  unrab  4236  inrab  4237  inrab2  4238  difrab  4239  dfrab3  4240  notrab  4242  rabun2  4244  dfnul3  4257  dfnul3OLD  4259  rab0  4313  rabeq0w  4314  rabeq0  4315  dfif6  4459  rabeqsn  4599  rabsssn  4600  rabsnifsb  4655  reusn  4660  rabsneu  4662  elunirab  4852  elintrab  4888  ssintrab  4899  iunrab  4978  iinrab  4994  intexrab  5259  rmorabex  5369  exss  5372  rabxp  5626  mptpreima  6130  setlikespec  6217  fndmin  6904  fncnvima2  6920  riotauni  7218  riotacl2  7229  snriota  7246  orduniss2  7655  exse2  7738  zfrep6  7771  xp2  7841  unielxp  7842  dfopab2  7865  suppvalbr  7952  ressuppss  7970  rankval3b  9515  scottexs  9576  scott0s  9577  kardex  9583  cardval2  9680  r0weon  9699  axdc2lem  10135  sstskm  10529  negfi  11854  nnzrab  12278  nn0zrab  12279  prprrab  14115  wrdnval  14176  cshwsexa  14465  shftlem  14707  shftuz  14708  shftdm  14710  hashbc0  16634  cshwsiun  16729  submacs  18380  eqglact  18722  cycsubg  18742  dfrhm2  19876  znunithash  20684  aspval2  21012  psrbaglefi  21045  psrbaglefiOLD  21046  clsval2  22109  xkoptsub  22713  ptcmplem2  23112  cnblcld  23844  cncmet  24391  shft2rab  24577  sca2rab  24581  vmappw  26170  2lgslem1b  26445  nb3grprlem1  27650  vtxdun  27751  rusgrprc  27860  ewlksfval  27871  wwlksnfi  28172  rusgrnumwwlkb0  28237  eclclwwlkn1  28340  clwwlkvbij  28378  h2hcau  29242  dfch2  29670  hhcno  30167  hhcnf  30168  pjhmopidm  30446  elpjrn  30453  dmrab  30745  rabfmpunirn  30892  mptctf  30954  maprnin  30968  fpwrelmapffslem  30969  fpwrelmap  30970  sigaex  31978  sigaval  31979  bnj1441  32720  bnj1441g  32721  bnj110  32738  fnrelpredd  32961  madeval2  33964  neibastop3  34478  bj-rababw  34993  bj-rabbida2  35033  bj-inrab  35042  rabiun  35677  ptrest  35703  poimirlem26  35730  poimirlem27  35731  cnambfre  35752  areacirclem5  35796  ispridlc  36155  eccnvepres  36342  lkrval2  37031  lfl1dim  37062  glbconxN  37319  dva1dim  38926  dib1dim2  39109  diclspsn  39135  dih1dimatlem  39270  dihglb2  39283  hdmapoc  39872  elrab2w  40095  prjspeclsp  40372  eq0rabdioph  40514  rexrabdioph  40532  eldioph4b  40549  aomclem4  40798  harval3  41041  alephiso2  41054  clcnvlem  41120  ntrneiel2  41585  scottabf  41747  rabexgf  42456  ssrabf  42553  rabssf  42557  rabbida2  42570  rabbida3  42573  f1oresf1o  44669  sprvalpw  44820  prprvalpw  44855  prprspr2  44858  submgmacs  45246  dfnrm2  46113  dfnrm3  46114