Definition df-rab 3074

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

This definition is referenced by:  rabid  3308  rabrab  3309  rabid2f  3311  rabid2OLD  3313  rabbi  3314  nfrab1  3315  nfrabw  3316  nfrabwOLD  3317  nfrab  3318  rabbiia  3404  rabbidva2  3408  rabeqf  3413  rabeqiOLD  3415  cbvrabw  3422  cbvrab  3423  cbvrabv  3424  rabrabi  3425  rabeqcda  3427  rabab  3458  elrabi  3619  elrabiOLD  3620  elrabf  3621  rabeqc  3623  elrab3t  3624  elrab  3625  ralrab2  3637  rexrab2  3640  cbvrabcsfw  3880  cbvrabcsf  3884  dfin5  3899  dfdif2  3900  ss2rab  4008  rabss  4009  ssrab  4010  rabss2  4015  ssrab2OLD  4018  rabssab  4022  notab  4243  unrab  4244  inrab  4245  inrab2  4246  difrab  4247  dfrab3  4248  notrab  4250  rabun2  4252  dfnul3  4265  dfnul3OLD  4267  rab0  4321  rabeq0w  4322  rabeq0  4323  dfif6  4467  rabeqsn  4607  rabsssn  4608  rabsnifsb  4663  reusn  4668  rabsneu  4670  elunirab  4860  elintrab  4896  ssintrab  4907  iunrab  4986  iinrab  5002  intexrab  5267  rmorabex  5377  exss  5380  rabxp  5634  mptpreima  6138  setlikespec  6225  predres  6239  fndmin  6916  fncnvima2  6932  riotauni  7231  riotacl2  7242  snriota  7259  orduniss2  7668  exse2  7751  zfrep6  7784  xp2  7854  unielxp  7855  dfopab2  7878  suppvalbr  7965  ressuppss  7983  rankval3b  9568  scottexs  9629  scott0s  9630  kardex  9636  cardval2  9733  r0weon  9752  axdc2lem  10188  sstskm  10582  negfi  11907  nnzrab  12331  nn0zrab  12332  prprrab  14168  wrdnval  14229  cshwsexa  14518  shftlem  14760  shftuz  14761  shftdm  14763  hashbc0  16687  cshwsiun  16782  submacs  18446  eqglact  18788  cycsubg  18808  dfrhm2  19942  znunithash  20753  aspval2  21083  psrbaglefi  21116  psrbaglefiOLD  21117  clsval2  22182  xkoptsub  22786  ptcmplem2  23185  cnblcld  23919  cncmet  24467  shft2rab  24653  sca2rab  24657  vmappw  26246  2lgslem1b  26521  nb3grprlem1  27728  vtxdun  27829  rusgrprc  27938  ewlksfval  27949  wwlksnfi  28250  rusgrnumwwlkb0  28315  eclclwwlkn1  28418  clwwlkvbij  28456  h2hcau  29320  dfch2  29748  hhcno  30245  hhcnf  30246  pjhmopidm  30524  elpjrn  30531  dmrab  30823  rabfmpunirn  30969  mptctf  31031  maprnin  31045  fpwrelmapffslem  31046  fpwrelmap  31047  sigaex  32057  sigaval  32058  bnj1441  32799  bnj1441g  32800  bnj110  32817  fnrelpredd  33040  madeval2  34016  neibastop3  34530  bj-rababw  35045  bj-rabbida2  35085  bj-inrab  35094  rabiun  35729  ptrest  35755  poimirlem26  35782  poimirlem27  35783  cnambfre  35804  areacirclem5  35848  ispridlc  36207  eccnvepres  36394  lkrval2  37083  lfl1dim  37114  glbconxN  37371  dva1dim  38978  dib1dim2  39161  diclspsn  39187  dih1dimatlem  39322  dihglb2  39335  hdmapoc  39924  elrab2w  40147  prjspeclsp  40431  eq0rabdioph  40578  rexrabdioph  40596  eldioph4b  40613  aomclem4  40862  harval3  41105  alephiso2  41118  clcnvlem  41184  ntrneiel2  41649  scottabf  41811  rabexgf  42520  ssrabf  42617  rabssf  42621  rabbida2  42634  rabbida3  42637  f1oresf1o  44733  sprvalpw  44884  prprvalpw  44919  prprspr2  44922  submgmacs  45310  dfnrm2  46177  dfnrm3  46178