Definition df-rab 3413

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 3077. (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 3412	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1568	. . . . 5 class 𝑥
6	5, 3	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2738	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1569	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is used by:  rabbidva2  3414  cbvrabv  3422  rabeqcda  3423  rabrabi  3430  nfrab1  3431  rabid  3432  rabbida4  3436  rabbi  3441  rabid2f  3442  rabid2im  3443  cbvrabw  3446  nfrabw  3447  nfrab  3448  cbvrab  3449  rabab  3480  elrabi  3640  elrabf  3641  elrab3t  3643  elrab  3644  elrab2w  3649  ralrab2  3655  rexrab2  3657  cbvrabcsfw  3887  cbvrabcsf  3891  ss2rab  3994  rabss  3995  ssrab  3996  ss2rabd  3997  rabss2  4002  rabss2OLD  4003  rabssab  4010  dfdif2  4048  dfin5  4092  notab  4259  unrab  4260  inrab  4261  inrab2  4262  difrab  4263  dfrab3  4264  notrab  4267  rabun2  4269  dfnul3  4282  rab0OLD  4335  rabeq0w  4336  rabeq0  4337  dfif6  4484  rabeqsn  4624  rabsssn  4625  rabsnifsb  4679  reusn  4684  rabsneu  4686  elunirab  4881  elintrab  4919  ssintrab  4930  iunrab  5010  iinrab  5026  intexrab  5307  rmorabex  5427  exss  5430  rabxp  5698  mptpreima  6239  setlikespec  6328  predres  6342  fndmin  7044  fncnvima2  7060  riotauni  7383  riotacl2  7393  snriota  7410  orduniss2  7844  exse2  7929  zfrep6OLD  7967  xp2  8038  unielxp  8039  dfopab2  8063  suppvalbr  8183  suppvalbrOLD  8184  ressuppss  8203  rankval3b  9839  scottabf  9942  scottexsOLD  9946  scott0bsOLD  9948  kardexOLD  9961  cardval2  10075  r0weon  10094  axdc2lem  10529  sstskm  10930  negfi  12269  nnzrab  12727  nn0zrab  12728  prprrab  14621  wrdnval  14693  shftlem  15226  shftuz  15227  shftdm  15229  hashbc0  17188  cshwsiun  17282  nfchnd  18790  submgmacs  18911  submacs  19028  eqglact  19396  cycsubg  19428  dfrhm2  20709  znunithash  21875  aspval2  22211  psrbaglefi  22239  clsval2  23373  xkoptsub  23978  ptcmplem2  24377  cnblcld  25098  cncmet  25648  shft2rab  25834  sca2rab  25838  vmappw  27448  2lgslem1b  27724  madeval2  28224  nb3grprlem1  29966  vtxdun  30067  rusgrprc  30176  ewlksfval  30187  wwlksnfi  30500  rusgrnumwwlkb0  30568  eclclwwlkn1  30671  clwwlkvbij  30709  h2hcau  31586  dfch2  32014  hhcno  32511  hhcnf  32512  pjhmopidm  32790  elpjrn  32797  dmrab  33140  rabsspr  33144  rabsstp  33145  rabfmpunirn  33294  mptctf  33355  maprnin  33369  fpwrelmapffslem  33370  fpwrelmap  33371  sigaex  34788  sigaval  34789  bnj1441  35516  bnj1441g  35517  bnj110  35534  fnrelpredd  35772  rabeqbii  37075  cbvrabdavw  37142  cbvrabdavw2  37166  neibastop3  37242  bj-rababw  37885  bj-inrab  37932  rabiun  38614  ptrest  38630  poimirlem26  38657  poimirlem27  38658  cnambfre  38679  areacirclem5  38723  ispridlc  39097  eqrabi  39281  ec1cnvres  39301  eccnvepres  39311  lkrval2  40240  lfl1dim  40271  glbconxN  40528  dva1dim  42135  dib1dim2  42318  diclspsn  42344  dih1dimatlem  42479  dihglb2  42492  hdmapoc  43081  sticksstones23  43312  aks6d1c6isolem3  43319  prjspeclsp  43733  eq0rabdioph  43880  rexrabdioph  43894  eldioph4b  43911  aomclem4  44152  onsucrn  44366  dfno2  44522  harval3  44632  alephiso2  44652  clcnvlem  44716  ntrneiel2  45179  rabexgf  46134  ssrabf  46222  rabssf  46227  cbvrabv2w  46236  rabbida2  46240  rabbida3  46243  f1oresf1o  48453  sprvalpw  48655  prprvalpw  48690  prprspr2  48693  stgr1  49152  dfnrm2  50139  dfnrm3  50140