Definition df-rab 3147

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 3143). (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 3142	. 2 class {𝑥 ∈ 𝐴 ∣ 𝜑}
5	2	cv 1536	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 398	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cab 2799	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
9	4, 8	wceq 1537	1 wff {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}

This definition is referenced by:  rabid  3378  rabrab  3379  rabid2  3381  rabid2f  3382  rabbi  3383  nfrab1  3384  nfrabw  3385  nfrab  3386  rabbiia  3472  rabbidva2  3476  rabeqf  3481  rabeqi  3482  cbvrabw  3489  cbvrab  3490  cbvrabv  3491  rabab  3523  elrabi  3675  elrabf  3676  rabeqc  3678  elrab3t  3679  elrab  3680  ralrab2  3690  rexrab2  3693  cbvrabcsfw  3924  cbvrabcsf  3928  dfin5  3944  dfdif2  3945  ss2rab  4047  rabss  4048  ssrab  4049  rabss2  4054  ssrab2  4056  rabssab  4060  notab  4273  unrab  4274  inrab  4275  inrab2  4276  difrab  4277  dfrab3  4278  notrab  4280  rabun2  4282  dfnul3  4295  rab0  4337  rabeq0  4338  dfif6  4470  rabeqsn  4606  rabsssn  4607  rabsnifsb  4658  reusn  4663  rabsneu  4665  elunirab  4854  elintrab  4888  ssintrab  4899  iunrab  4976  iinrab  4991  intexrab  5243  rmorabex  5352  exss  5355  rabxp  5600  mptpreima  6092  setlikespec  6169  fndmin  6815  fncnvima2  6831  riotauni  7120  riotacl2  7130  snriota  7147  orduniss2  7548  exse2  7622  zfrep6  7656  xp2  7726  unielxp  7727  dfopab2  7750  suppvalbr  7834  ressuppss  7849  rankval3b  9255  scottexs  9316  scott0s  9317  kardex  9323  cardval2  9420  r0weon  9438  axdc2lem  9870  sstskm  10264  negfi  11589  nnzrab  12011  nn0zrab  12012  prprrab  13832  wrdnval  13896  cshwsexa  14186  shftlem  14427  shftuz  14428  shftdm  14430  hashbc0  16341  cshwsiun  16433  submacs  17991  eqglact  18331  cycsubg  18351  dfrhm2  19469  aspval2  20127  psrbaglefi  20152  znunithash  20711  clsval2  21658  xkoptsub  22262  ptcmplem2  22661  cnblcld  23383  cncmet  23925  shft2rab  24109  sca2rab  24113  vmappw  25693  2lgslem1b  25968  nb3grprlem1  27162  vtxdun  27263  rusgrprc  27372  ewlksfval  27383  wwlksnfi  27684  wwlksnfiOLD  27685  rusgrnumwwlkb0  27750  eclclwwlkn1  27854  clwwlkvbij  27892  h2hcau  28756  dfch2  29184  hhcno  29681  hhcnf  29682  pjhmopidm  29960  elpjrn  29967  dmrab  30260  rabfmpunirn  30398  mptctf  30453  maprnin  30467  fpwrelmapffslem  30468  fpwrelmap  30469  sigaex  31369  sigaval  31370  bnj1441  32112  bnj1441g  32113  bnj110  32130  madeval2  33290  neibastop3  33710  bj-rababw  34200  bj-rabbida2  34240  bj-inrab  34248  rabiun  34880  ptrest  34906  poimirlem26  34933  poimirlem27  34934  cnambfre  34955  areacirclem5  35001  ispridlc  35363  eccnvepres  35552  lkrval2  36241  lfl1dim  36272  glbconxN  36529  dva1dim  38136  dib1dim2  38319  diclspsn  38345  dih1dimatlem  38480  dihglb2  38493  hdmapoc  39082  rabeqcda  39155  prjspeclsp  39311  eq0rabdioph  39422  rexrabdioph  39440  eldioph4b  39457  aomclem4  39706  harval3  39953  alephiso2  39966  clcnvlem  40032  ntrneiel2  40485  scottabf  40625  rabexgf  41330  ssrabf  41430  rabssf  41434  rabbida2  41448  rabbida3  41451  f1oresf1o  43538  sprvalpw  43691  prprvalpw  43726  prprspr2  43729  submgmacs  44120