Definition df-rab 3116

Description: Define a restricted class abstraction (class builder), which is the class of all 𝑥 in 𝐴 such that 𝜑 is true. Definition of [TakeutiZaring] p. 20.

Note: For the reading given above Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint.

Should instead 𝐴 depend on 𝑥, you rather get a class of all those 𝑥 fulfilling 𝜑 that happen to be contained in the corresponding 𝐴(𝑥). This need not be a subset of any of the 𝐴(𝑥) at all. Such interpretation is rarely needed (see also df-ral 3112). (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 3111	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1524	. . . . 5 class 𝑥
6	5, 3	wcel 2083	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 396	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2777	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1525	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  3339  rabrab  3340  rabid2  3342  rabid2f  3343  rabbi  3344  rabswap  3345  nfrab1  3346  nfrab  3347  rabbiia  3420  rabbidva2  3424  rabeqf  3429  rabeqi  3430  cbvrab  3436  cbvrabv  3437  rabab  3469  elrabi  3616  elrabf  3617  rabeqc  3619  elrab3t  3620  elrab  3621  ralrab2  3631  rexrab2  3634  cbvrabcsf  3858  dfin5  3873  dfdif2  3874  ss2rab  3974  rabss  3975  ssrab  3976  rabss2  3981  ssrab2  3983  rabssab  3987  notab  4199  unrab  4200  inrab  4201  inrab2  4202  difrab  4203  dfrab3  4204  notrab  4206  rabun2  4208  dfnul3  4221  rab0  4263  rabeq0  4264  dfif6  4390  rabeqsn  4517  rabsssn  4518  rabsnifsb  4571  reusn  4576  rabsneu  4578  elunirab  4763  elintrab  4800  ssintrab  4811  iunrab  4881  iinrab  4896  intexrab  5141  rmorabex  5251  exss  5254  rabxp  5495  mptpreima  5974  setlikespec  6051  fndmin  6687  fncnvima2  6703  riotauni  6990  riotacl2  6997  snriota  7014  orduniss2  7411  exse2  7485  zfrep6  7519  xp2  7589  unielxp  7590  dfopab2  7613  suppvalbr  7692  ressuppss  7707  rankval3b  9108  scottexs  9169  scott0s  9170  kardex  9176  cardval2  9273  r0weon  9291  axdc2lem  9723  sstskm  10117  negfi  11443  nnzrab  11864  nn0zrab  11865  prprrab  13681  wrdnval  13746  cshwsexa  14026  shftlem  14265  shftuz  14266  shftdm  14268  hashbc0  16174  cshwsiun  16266  submacs  17808  cycsubg  18065  eqglact  18088  dfrhm2  19163  aspval2  19819  psrbaglefi  19844  znunithash  20397  clsval2  21346  xkoptsub  21950  ptcmplem2  22349  cnblcld  23070  cncmet  23612  shft2rab  23796  sca2rab  23800  vmappw  25379  2lgslem1b  25654  nb3grprlem1  26849  vtxdun  26950  rusgrprc  27059  ewlksfval  27070  wwlksnfi  27370  wwlksnfiOLD  27371  rusgrnumwwlkb0  27436  eclclwwlkn1  27540  clwwlkvbij  27578  h2hcau  28443  dfch2  28871  hhcno  29368  hhcnf  29369  pjhmopidm  29647  elpjrn  29654  dmrab  29948  rabfmpunirn  30084  mptctf  30137  maprnin  30151  fpwrelmapffslem  30152  fpwrelmap  30153  sigaex  30982  sigaval  30983  bnj1441  31725  bnj110  31742  madeval2  32901  neibastop3  33321  bj-rababw  33775  bj-rabbida2  33814  bj-inrab  33822  rabiun  34417  ptrest  34443  poimirlem26  34470  poimirlem27  34471  cnambfre  34492  areacirclem5  34538  ispridlc  34901  eccnvepres  35090  lkrval2  35778  lfl1dim  35809  glbconxN  36066  dva1dim  37673  dib1dim2  37856  diclspsn  37882  dih1dimatlem  38017  dihglb2  38030  hdmapoc  38619  rabeqcda  38657  prjspeclsp  38780  eq0rabdioph  38879  rexrabdioph  38897  eldioph4b  38914  aomclem4  39163  harval3  39410  alephiso2  39423  clcnvlem  39489  ntrneiel2  39942  scottabf  40094  rabexgf  40841  ssrabf  40942  rabssf  40946  rabbida2  40959  rabbida3  40962  f1oresf1o  43027  sprvalpw  43146  prprvalpw  43181  prprspr2  43184  submgmacs  43575