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 3118
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 3114. (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 3113 . 2 class {𝑥𝐴𝜑}
52cv 1537 . . . . 5 class 𝑥
65, 3wcel 2112 . . . 4 wff 𝑥𝐴
76, 1wa 399 . . 3 wff (𝑥𝐴𝜑)
87, 2cab 2779 . 2 class {𝑥 ∣ (𝑥𝐴𝜑)}
94, 8wceq 1538 1 wff {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  rabid  3334  rabrab  3335  rabid2  3337  rabid2f  3338  rabbi  3339  nfrab1  3340  nfrabw  3341  nfrab  3342  rabbiia  3422  rabbidva2  3426  rabeqf  3431  rabeqiOLD  3433  cbvrabw  3440  cbvrab  3441  cbvrabv  3442  rabab  3473  elrabi  3626  elrabf  3627  rabeqc  3629  elrab3t  3630  elrab  3631  ralrab2  3641  rexrab2  3644  cbvrabcsfw  3872  cbvrabcsf  3876  dfin5  3892  dfdif2  3893  ss2rab  4001  rabss  4002  ssrab  4003  rabss2  4008  ssrab2  4010  rabssab  4014  notab  4228  unrab  4229  inrab  4230  inrab2  4231  difrab  4232  dfrab3  4233  notrab  4235  rabun2  4237  dfnul3  4249  rab0  4294  rabeq0  4295  dfif6  4431  rabeqsn  4569  rabsssn  4570  rabsnifsb  4621  reusn  4626  rabsneu  4628  elunirab  4819  elintrab  4853  ssintrab  4864  iunrab  4942  iinrab  4957  intexrab  5210  rmorabex  5320  exss  5323  rabxp  5568  mptpreima  6063  setlikespec  6141  fndmin  6796  fncnvima2  6812  riotauni  7103  riotacl2  7113  snriota  7130  orduniss2  7532  exse2  7608  zfrep6  7642  xp2  7712  unielxp  7713  dfopab2  7736  suppvalbr  7821  ressuppss  7836  rankval3b  9243  scottexs  9304  scott0s  9305  kardex  9311  cardval2  9408  r0weon  9427  axdc2lem  9863  sstskm  10257  negfi  11581  nnzrab  12002  nn0zrab  12003  prprrab  13831  wrdnval  13892  cshwsexa  14181  shftlem  14422  shftuz  14423  shftdm  14425  hashbc0  16334  cshwsiun  16428  submacs  17986  eqglact  18326  cycsubg  18346  dfrhm2  19468  znunithash  20259  aspval2  20587  psrbaglefi  20613  clsval2  21658  xkoptsub  22262  ptcmplem2  22661  cnblcld  23383  cncmet  23929  shft2rab  24115  sca2rab  24119  vmappw  25704  2lgslem1b  25979  nb3grprlem1  27173  vtxdun  27274  rusgrprc  27383  ewlksfval  27394  wwlksnfi  27695  rusgrnumwwlkb0  27760  eclclwwlkn1  27863  clwwlkvbij  27901  h2hcau  28765  dfch2  29193  hhcno  29690  hhcnf  29691  pjhmopidm  29969  elpjrn  29976  dmrab  30270  rabfmpunirn  30419  mptctf  30482  maprnin  30496  fpwrelmapffslem  30497  fpwrelmap  30498  sigaex  31477  sigaval  31478  bnj1441  32220  bnj1441g  32221  bnj110  32238  madeval2  33398  neibastop3  33818  bj-rababw  34316  bj-rabbida2  34356  bj-inrab  34364  rabiun  35023  ptrest  35049  poimirlem26  35076  poimirlem27  35077  cnambfre  35098  areacirclem5  35142  ispridlc  35501  eccnvepres  35690  lkrval2  36379  lfl1dim  36410  glbconxN  36667  dva1dim  38274  dib1dim2  38457  diclspsn  38483  dih1dimatlem  38618  dihglb2  38631  hdmapoc  39220  rabeqcda  39385  prjspeclsp  39593  eq0rabdioph  39704  rexrabdioph  39722  eldioph4b  39739  aomclem4  39988  harval3  40231  alephiso2  40244  clcnvlem  40310  ntrneiel2  40776  scottabf  40935  rabexgf  41640  ssrabf  41737  rabssf  41741  rabbida2  41755  rabbida3  41758  f1oresf1o  43833  sprvalpw  43984  prprvalpw  44019  prprspr2  44022  submgmacs  44411
  Copyright terms: Public domain W3C validator