Definition df-rab 3418

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 3080. (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 3417	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1562	. . . . 5 class 𝑥
6	5, 3	wcel 2145	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 400	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2743	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1563	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabbidva2  3419  cbvrabv  3427  rabeqcda  3428  rabrabi  3436  nfrab1  3437  rabid  3438  rabbida4  3442  rabbi  3447  rabid2f  3448  rabid2im  3449  cbvrabw  3452  cbvrabwOLD  3453  nfrabw  3454  nfrab  3455  cbvrab  3456  rabab  3487  elrabi  3649  elrabf  3650  elrab3t  3652  elrab  3653  elrab2w  3658  ralrab2  3664  rexrab2  3666  cbvrabcsfw  3896  cbvrabcsf  3900  dfin5  3915  dfdif2  3916  ss2rab  4025  rabss  4026  ssrab  4027  ss2rabd  4028  rabss2  4033  rabss2OLD  4034  rabssab  4041  notab  4269  unrab  4270  inrab  4271  inrab2  4272  difrab  4273  dfrab3  4274  notrab  4277  rabun2  4279  dfnul3  4292  rab0OLD  4343  rabeq0w  4344  rabeq0  4345  dfif6  4486  rabeqsn  4629  rabsssn  4630  rabsnifsb  4684  reusn  4689  rabsneu  4691  elunirab  4883  elintrab  4921  ssintrab  4932  iunrab  5013  iinrab  5029  intexrab  5308  rmorabex  5432  exss  5435  rabxp  5700  mptpreima  6229  setlikespec  6316  predres  6330  fndmin  7030  fncnvima2  7046  riotauni  7363  riotacl2  7373  snriota  7390  orduniss2  7817  exse2  7902  zfrep6OLD  7940  xp2  8011  unielxp  8012  dfopab2  8037  suppvalbr  8148  ressuppss  8167  rankval3b  9786  scottexs  9849  scott0s  9850  scottabf  9854  kardex  9868  cardval2  9965  r0weon  9984  axdc2lem  10420  sstskm  10815  negfi  12155  nnzrab  12613  nn0zrab  12614  prprrab  14500  wrdnval  14572  shftlem  15095  shftuz  15096  shftdm  15098  hashbc0  17055  cshwsiun  17149  nfchnd  18657  submgmacs  18765  submacs  18876  eqglact  19238  cycsubg  19270  dfrhm2  20547  znunithash  21674  aspval2  22008  psrbaglefi  22036  clsval2  23168  xkoptsub  23772  ptcmplem2  24171  cnblcld  24892  cncmet  25442  shft2rab  25628  sca2rab  25632  vmappw  27238  2lgslem1b  27514  madeval2  27984  nb3grprlem1  29639  vtxdun  29740  rusgrprc  29849  ewlksfval  29860  wwlksnfi  30164  rusgrnumwwlkb0  30232  eclclwwlkn1  30335  clwwlkvbij  30373  h2hcau  31240  dfch2  31668  hhcno  32165  hhcnf  32166  pjhmopidm  32444  elpjrn  32451  dmrab  32753  rabsspr  32757  rabsstp  32758  rabfmpunirn  32910  mptctf  32973  maprnin  32988  fpwrelmapffslem  32989  fpwrelmap  32990  sigaex  34417  sigaval  34418  bnj1441  35145  bnj1441g  35146  bnj110  35163  fnrelpredd  35397  rabeqbii  36567  cbvrabdavw  36634  cbvrabdavw2  36658  neibastop3  36735  bj-rababw  37378  bj-inrab  37424  rabiun  38104  ptrest  38130  poimirlem26  38157  poimirlem27  38158  cnambfre  38179  areacirclem5  38223  ispridlc  38581  eqrabi  38767  ec1cnvres  38787  eccnvepres  38797  lkrval2  39726  lfl1dim  39757  glbconxN  40014  dva1dim  41621  dib1dim2  41804  diclspsn  41830  dih1dimatlem  41965  dihglb2  41978  hdmapoc  42567  sticksstones23  42798  aks6d1c6isolem3  42805  prjspeclsp  43206  eq0rabdioph  43369  rexrabdioph  43383  eldioph4b  43400  aomclem4  43646  onsucrn  43860  dfno2  44016  harval3  44126  alephiso2  44146  clcnvlem  44211  ntrneiel2  44674  rabexgf  45602  ssrabf  45690  rabssf  45695  cbvrabv2w  45704  rabbida2  45708  rabbida3  45711  f1oresf1o  47882  sprvalpw  48084  prprvalpw  48119  prprspr2  48122  stgr1  48581  dfnrm2  49561  dfnrm3  49562