Definition df-rab 3417

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

This definition is used by:  rabbidva2  3418  cbvrabv  3426  rabeqcda  3427  rabrabi  3434  nfrab1  3435  rabid  3436  rabbida4  3440  rabbi  3445  rabid2f  3446  rabid2im  3447  cbvrabw  3450  nfrabw  3451  nfrab  3452  cbvrab  3453  rabab  3484  elrabi  3644  elrabf  3645  elrab3t  3647  elrab  3648  elrab2w  3653  ralrab2  3659  rexrab2  3661  cbvrabcsfw  3892  cbvrabcsf  3896  ss2rab  3997  rabss  3998  ssrab  3999  ss2rabd  4000  rabss2  4005  rabss2OLD  4006  rabssab  4013  dfdif2  4051  dfin5  4095  notab  4262  unrab  4263  inrab  4264  inrab2  4265  difrab  4266  dfrab3  4267  notrab  4270  rabun2  4272  dfnul3  4285  rab0OLD  4339  rabeq0w  4340  rabeq0  4341  dfif6  4488  rabeqsn  4628  rabsssn  4629  rabsnifsb  4683  reusn  4688  rabsneu  4690  elunirab  4885  elintrab  4923  ssintrab  4934  iunrab  5014  iinrab  5030  intexrab  5312  rmorabex  5432  exss  5435  rabxp  5703  mptpreima  6252  setlikespec  6346  predres  6360  fndmin  7067  fncnvima2  7084  riotauni  7406  riotacl2  7416  snriota  7433  orduniss2  7868  exse2  7953  zfrep6OLD  7991  xp2  8062  unielxp  8063  dfopab2  8088  suppvalbr  8208  suppvalbrOLD  8209  ressuppss  8228  rankval3b  9863  scottabf  9966  scottexsOLD  9970  scott0bsOLD  9972  kardexOLD  9985  cardval2  10099  r0weon  10118  axdc2lem  10553  sstskm  10954  negfi  12293  nnzrab  12751  nn0zrab  12752  prprrab  14645  wrdnval  14717  shftlem  15250  shftuz  15251  shftdm  15253  hashbc0  17212  cshwsiun  17306  nfchnd  18814  submgmacs  18935  submacs  19052  eqglact  19420  cycsubg  19452  dfrhm2  20734  znunithash  21900  aspval2  22236  psrbaglefi  22264  clsval2  23398  xkoptsub  24003  ptcmplem2  24402  cnblcld  25123  cncmet  25673  shft2rab  25859  sca2rab  25863  vmappw  27473  2lgslem1b  27749  madeval2  28249  nb3grprlem1  29991  vtxdun  30092  rusgrprc  30201  ewlksfval  30212  wwlksnfi  30525  rusgrnumwwlkb0  30593  eclclwwlkn1  30696  clwwlkvbij  30734  h2hcau  31611  dfch2  32039  hhcno  32536  hhcnf  32537  pjhmopidm  32815  elpjrn  32822  dmrab  33165  rabsspr  33169  rabsstp  33170  rabfmpunirn  33319  mptctf  33379  maprnin  33393  fpwrelmapffslem  33394  fpwrelmap  33395  sigaex  34812  sigaval  34813  bnj1441  35540  bnj1441g  35541  bnj110  35558  fnrelpredd  35804  rabeqbii  37161  cbvrabdavw  37228  cbvrabdavw2  37252  neibastop3  37328  bj-rababw  37971  bj-inrab  38018  rabiun  38713  ptrest  38729  poimirlem26  38756  poimirlem27  38757  cnambfre  38778  areacirclem5  38822  ispridlc  39196  eqrabi  39380  ec1cnvres  39400  eccnvepres  39410  lkrval2  40339  lfl1dim  40370  glbconxN  40627  dva1dim  42234  dib1dim2  42417  diclspsn  42443  dih1dimatlem  42578  dihglb2  42591  hdmapoc  43180  sticksstones23  43411  aks6d1c6isolem3  43418  prjspeclsp  43833  eq0rabdioph  43980  rexrabdioph  43994  eldioph4b  44011  aomclem4  44252  onsucrn  44465  dfno2  44621  harval3  44731  alephiso2  44751  clcnvlem  44815  ntrneiel2  45278  rabexgf  46246  ssrabf  46334  rabssf  46339  cbvrabv2w  46348  rabbida2  46352  rabbida3  46355  f1oresf1o  48565  sprvalpw  48767  prprvalpw  48802  prprspr2  48805  stgr1  49264  dfnrm2  50251  dfnrm3  50252