Definition df-rab 3434

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 3063. (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 3433	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1541	. . . . 5 class 𝑥
6	5, 3	wcel 2107	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 397	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2710	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1542	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3435  rabbiiaOLD  3438  cbvrabv  3443  rabeqcda  3444  rabrabi  3451  nfrab1  3452  rabid  3453  rabrab  3456  rabbida4  3458  rabbi  3463  rabid2f  3464  rabid2OLD  3466  rabeqf  3467  cbvrabw  3468  nfrabw  3469  nfrabwOLD  3470  rabeqiOLD  3472  nfrab  3473  cbvrab  3474  rabab  3503  elrabi  3677  elrabiOLD  3678  elrabf  3679  rabeqcOLD  3681  elrab3t  3682  elrab  3683  ralrab2  3694  rexrab2  3696  cbvrabcsfw  3937  cbvrabcsf  3941  dfin5  3956  dfdif2  3957  ss2rab  4068  rabss  4069  ssrab  4070  rabss2  4075  ssrab2OLD  4078  rabssab  4083  notab  4304  unrab  4305  inrab  4306  inrab2  4307  difrab  4308  dfrab3  4309  notrab  4311  rabun2  4313  dfnul3  4326  dfnul3OLD  4328  rab0  4382  rabeq0w  4383  rabeq0  4384  dfif6  4531  rabeqsn  4669  rabsssn  4670  rabsnifsb  4726  reusn  4731  rabsneu  4733  elunirab  4924  elintrab  4964  ssintrab  4975  iunrab  5055  iinrab  5072  intexrab  5340  rmorabex  5460  exss  5463  rabxp  5723  mptpreima  6235  setlikespec  6324  predres  6338  fndmin  7044  fncnvima2  7060  riotauni  7368  riotacl2  7379  snriota  7396  orduniss2  7818  exse2  7905  zfrep6  7938  xp2  8009  unielxp  8010  dfopab2  8035  suppvalbr  8147  ressuppss  8165  rankval3b  9818  scottexs  9879  scott0s  9880  kardex  9886  cardval2  9983  r0weon  10004  axdc2lem  10440  sstskm  10834  negfi  12160  nnzrab  12587  nn0zrab  12588  prprrab  14431  wrdnval  14492  cshwsexaOLD  14772  shftlem  15012  shftuz  15013  shftdm  15015  hashbc0  16935  cshwsiun  17030  submacs  18705  eqglact  19054  cycsubg  19080  dfrhm2  20246  znunithash  21112  aspval2  21444  psrbaglefi  21477  psrbaglefiOLD  21478  clsval2  22546  xkoptsub  23150  ptcmplem2  23549  cnblcld  24283  cncmet  24831  shft2rab  25017  sca2rab  25021  vmappw  26610  2lgslem1b  26885  madeval2  27338  nb3grprlem1  28627  vtxdun  28728  rusgrprc  28837  ewlksfval  28848  wwlksnfi  29150  rusgrnumwwlkb0  29215  eclclwwlkn1  29318  clwwlkvbij  29356  h2hcau  30220  dfch2  30648  hhcno  31145  hhcnf  31146  pjhmopidm  31424  elpjrn  31431  dmrab  31725  rabfmpunirn  31866  mptctf  31930  maprnin  31944  fpwrelmapffslem  31945  fpwrelmap  31946  sigaex  33097  sigaval  33098  bnj1441  33840  bnj1441g  33841  bnj110  33858  fnrelpredd  34081  neibastop3  35236  bj-rababw  35750  bj-inrab  35796  rabiun  36450  ptrest  36476  poimirlem26  36503  poimirlem27  36504  cnambfre  36525  areacirclem5  36569  ispridlc  36927  eccnvepres  37137  lkrval2  37949  lfl1dim  37980  glbconxN  38238  dva1dim  39845  dib1dim2  40028  diclspsn  40054  dih1dimatlem  40189  dihglb2  40202  hdmapoc  40791  elrab2w  41016  prjspeclsp  41351  eq0rabdioph  41500  rexrabdioph  41518  eldioph4b  41535  aomclem4  41785  onsucrn  42007  dfno2  42165  harval3  42275  alephiso2  42295  clcnvlem  42360  ntrneiel2  42823  scottabf  42985  rabexgf  43694  ssrabf  43789  rabssf  43794  rabbida2  43807  rabbida3  43810  f1oresf1o  45985  sprvalpw  46135  prprvalpw  46170  prprspr2  46173  submgmacs  46561  dfnrm2  47518  dfnrm3  47519