Definition df-rab 3394

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 3046. (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 3393	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2110	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2708	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1541	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3395  cbvrabv  3403  rabeqcda  3404  rabrabi  3412  nfrab1  3413  rabid  3414  rabrab  3417  rabbida4  3418  rabbi  3423  rabid2f  3424  rabid2im  3425  rabeqf  3427  cbvrabw  3428  cbvrabwOLD  3429  nfrabw  3430  nfrab  3432  cbvrab  3433  rabab  3465  elrabi  3641  elrabf  3642  elrab3t  3644  elrab  3645  elrab2w  3649  ralrab2  3655  rexrab2  3657  cbvrabcsfw  3889  cbvrabcsf  3893  dfin5  3908  dfdif2  3909  ss2rab  4019  rabss  4020  ssrab  4021  rabss2  4026  rabssab  4033  notab  4262  unrab  4263  inrab  4264  inrab2  4265  difrab  4266  dfrab3  4267  notrab  4270  rabun2  4272  dfnul3  4285  rab0  4334  rabeq0w  4335  rabeq0  4336  dfif6  4476  rabsneq  4593  rabeqsn  4618  rabsssn  4619  rabsnifsb  4673  reusn  4678  rabsneu  4680  elunirab  4872  elintrab  4908  ssintrab  4919  iunrab  4999  iinrab  5015  intexrab  5283  rmorabex  5398  exss  5401  rabxp  5662  mptpreima  6182  setlikespec  6268  predres  6282  fndmin  6973  fncnvima2  6989  riotauni  7304  riotacl2  7314  snriota  7331  orduniss2  7758  exse2  7842  zfrep6  7882  xp2  7953  unielxp  7954  dfopab2  7979  suppvalbr  8089  ressuppss  8108  rankval3b  9711  scottexs  9772  scott0s  9773  kardex  9779  cardval2  9876  r0weon  9895  axdc2lem  10331  sstskm  10725  negfi  12063  nnzrab  12492  nn0zrab  12493  prprrab  14372  wrdnval  14444  shftlem  14967  shftuz  14968  shftdm  14970  hashbc0  16909  cshwsiun  17003  nfchnd  18509  submgmacs  18617  submacs  18727  eqglact  19084  cycsubg  19113  dfrhm2  20385  znunithash  21494  aspval2  21828  psrbaglefi  21856  clsval2  22958  xkoptsub  23562  ptcmplem2  23961  cnblcld  24682  cncmet  25242  shft2rab  25429  sca2rab  25433  vmappw  27046  2lgslem1b  27323  madeval2  27787  nb3grprlem1  29351  vtxdun  29453  rusgrprc  29562  ewlksfval  29573  wwlksnfi  29877  rusgrnumwwlkb0  29942  eclclwwlkn1  30045  clwwlkvbij  30083  h2hcau  30949  dfch2  31377  hhcno  31874  hhcnf  31875  pjhmopidm  32153  elpjrn  32160  dmrab  32466  rabsspr  32471  rabsstp  32472  rabfmpunirn  32625  mptctf  32689  maprnin  32704  fpwrelmapffslem  32705  fpwrelmap  32706  sigaex  34113  sigaval  34114  bnj1441  34842  bnj1441g  34843  bnj110  34860  fnrelpredd  35091  rabeqbii  36207  cbvrabdavw  36274  cbvrabdavw2  36298  neibastop3  36375  bj-rababw  36894  bj-inrab  36940  rabiun  37612  ptrest  37638  poimirlem26  37665  poimirlem27  37666  cnambfre  37687  areacirclem5  37731  ispridlc  38089  eccnvepres  38293  lkrval2  39108  lfl1dim  39139  glbconxN  39396  dva1dim  41003  dib1dim2  41186  diclspsn  41212  dih1dimatlem  41347  dihglb2  41360  hdmapoc  41949  sticksstones23  42181  aks6d1c6isolem3  42188  prjspeclsp  42624  eq0rabdioph  42788  rexrabdioph  42806  eldioph4b  42823  aomclem4  43069  onsucrn  43283  dfno2  43440  harval3  43550  alephiso2  43570  clcnvlem  43635  ntrneiel2  44098  scottabf  44252  rabexgf  45040  ssrabf  45130  rabssf  45135  cbvrabv2w  45144  rabbida2  45148  rabbida3  45151  f1oresf1o  47300  sprvalpw  47490  prprvalpw  47525  prprspr2  47528  stgr1  47971  dfnrm2  48942  dfnrm3  48943