MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rab Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3crab 3142 . 2 class {𝑥𝐴𝜑}
52cv 1527 . . . . 5 class 𝑥
65, 3wcel 2105 . . . 4 wff 𝑥𝐴
76, 1wa 396 . . 3 wff (𝑥𝐴𝜑)
87, 2cab 2799 . 2 class {𝑥 ∣ (𝑥𝐴𝜑)}
94, 8wceq 1528 1 wff {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  rabid  3379  rabrab  3380  rabid2  3382  rabid2f  3383  rabbi  3384  nfrab1  3385  nfrabw  3386  nfrab  3387  rabbiia  3473  rabbidva2  3477  rabeqf  3482  rabeqi  3483  cbvrabw  3490  cbvrab  3491  cbvrabv  3492  rabab  3524  elrabi  3674  elrabf  3675  rabeqc  3677  elrab3t  3678  elrab  3679  ralrab2  3689  rexrab2  3692  cbvrabcsfw  3923  cbvrabcsf  3927  dfin5  3943  dfdif2  3944  ss2rab  4046  rabss  4047  ssrab  4048  rabss2  4053  ssrab2  4055  rabssab  4059  notab  4272  unrab  4273  inrab  4274  inrab2  4275  difrab  4276  dfrab3  4277  notrab  4279  rabun2  4281  dfnul3  4294  rab0  4336  rabeq0  4337  dfif6  4468  rabeqsn  4598  rabsssn  4599  rabsnifsb  4652  reusn  4657  rabsneu  4659  elunirab  4844  elintrab  4881  ssintrab  4892  iunrab  4968  iinrab  4983  intexrab  5235  rmorabex  5344  exss  5347  rabxp  5594  mptpreima  6086  setlikespec  6163  fndmin  6808  fncnvima2  6824  riotauni  7109  riotacl2  7119  snriota  7136  orduniss2  7536  exse2  7610  zfrep6  7647  xp2  7717  unielxp  7718  dfopab2  7741  suppvalbr  7825  ressuppss  7840  rankval3b  9244  scottexs  9305  scott0s  9306  kardex  9312  cardval2  9409  r0weon  9427  axdc2lem  9859  sstskm  10253  negfi  11578  nnzrab  11999  nn0zrab  12000  prprrab  13821  wrdnval  13886  cshwsexa  14176  shftlem  14417  shftuz  14418  shftdm  14420  hashbc0  16331  cshwsiun  16423  submacs  17981  eqglact  18271  cycsubg  18291  dfrhm2  19400  aspval2  20057  psrbaglefi  20082  znunithash  20641  clsval2  21588  xkoptsub  22192  ptcmplem2  22591  cnblcld  23312  cncmet  23854  shft2rab  24038  sca2rab  24042  vmappw  25621  2lgslem1b  25896  nb3grprlem1  27090  vtxdun  27191  rusgrprc  27300  ewlksfval  27311  wwlksnfi  27612  wwlksnfiOLD  27613  rusgrnumwwlkb0  27678  eclclwwlkn1  27782  clwwlkvbij  27820  h2hcau  28684  dfch2  29112  hhcno  29609  hhcnf  29610  pjhmopidm  29888  elpjrn  29895  dmrab  30188  rabfmpunirn  30327  mptctf  30380  maprnin  30394  fpwrelmapffslem  30395  fpwrelmap  30396  sigaex  31269  sigaval  31270  bnj1441  32012  bnj1441g  32013  bnj110  32030  madeval2  33188  neibastop3  33608  bj-rababw  34095  bj-rabbida2  34135  bj-inrab  34143  rabiun  34747  ptrest  34773  poimirlem26  34800  poimirlem27  34801  cnambfre  34822  areacirclem5  34868  ispridlc  35231  eccnvepres  35420  lkrval2  36108  lfl1dim  36139  glbconxN  36396  dva1dim  38003  dib1dim2  38186  diclspsn  38212  dih1dimatlem  38347  dihglb2  38360  hdmapoc  38949  rabeqcda  38986  prjspeclsp  39142  eq0rabdioph  39253  rexrabdioph  39271  eldioph4b  39288  aomclem4  39537  harval3  39784  alephiso2  39797  clcnvlem  39863  ntrneiel2  40316  scottabf  40456  rabexgf  41161  ssrabf  41262  rabssf  41266  rabbida2  41279  rabbida3  41282  f1oresf1o  43370  sprvalpw  43489  prprvalpw  43524  prprspr2  43527  submgmacs  43918
  Copyright terms: Public domain W3C validator