MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rgenw Unicode version

Theorem rgenw 2818
Description: Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rgenw.1
Assertion
Ref Expression
rgenw

Proof of Theorem rgenw
StepHypRef Expression
1 rgenw.1 . . 3
21a1i 11 . 2
32rgen 2817 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818  A.wral 2807
This theorem is referenced by:  rgen2w  2819  reuun1  3779  riinrab  4406  0disj  4445  iinexg  4612  epse  4867  xpiindi  5143  eliunxp  5145  opeliunxp2  5146  elrnmpti  5258  fnmpti  5714  eqfnfv  5981  eufnfv  6146  mpt2eq12  6357  porpss  6584  iunex  6780  mpt2ex  6877  suppssov1  6951  suppssfv  6955  onnseq  7034  ixpssmap  7523  boxcutc  7532  nneneq  7720  finsschain  7847  dfom3  8085  cantnfdm  8102  cantnfdmOLD  8104  cantnfOLD  8155  rankuni2b  8292  rankval4  8306  alephf1  8487  dfac4  8524  dfacacn  8542  infmap2  8619  cfeq0  8657  fin23lem28  8741  axdc2lem  8849  axcclem  8858  ac6  8881  iundom  8938  konigthlem  8964  iunctb  8970  tskmid  9239  supmul1  10533  supmullem2  10535  supmul  10536  uzf  11113  seqof  12164  hashbclem  12501  wrdexg  12557  rlimclim1  13368  fsumcom2  13589  ackbijnn  13640  fprodcom2  13788  sumhash  14415  ramcl  14547  prdsval  14852  prdsbas  14854  prdshom  14864  imasplusg  14914  imasmulr  14915  imasvsca  14917  imasip  14918  imasaddfnlem  14925  imasvscafn  14934  isfunc  15233  wunfunc  15268  isnat  15316  natffn  15318  wunnat  15325  fucsect  15341  setcepi  15415  dfod2  16586  ghmcyg  16898  gsum2d2lem  17001  gsum2d2  17002  gsumcom2  17003  dmdprd  17029  dprdval  17034  dprdvalOLD  17036  dprdf11  17063  dprdf11OLD  17070  dprd2d2  17093  dpjeq  17108  dpjeqOLD  17115  pgpfac1lem2  17126  pgpfac1lem3  17128  pgpfac1lem4  17129  mptscmfsupp0  17576  00lsp  17627  ocv0  18708  ofco2  18953  tgidm  19482  pptbas  19509  tgrest  19660  iscnp2  19740  ist1-3  19850  discmp  19898  1stcfb  19946  lly1stc  19997  disllycmp  19999  dis1stc  20000  comppfsc  20033  txbas  20068  ptbasfi  20082  ptpjopn  20113  dfac14  20119  ptrescn  20140  xkoptsub  20155  fclsval  20509  ptcmplem2  20553  ptcmplem3  20554  cnextrel  20563  tsmsfbas  20626  ustuqtop  20749  prdsxmetlem  20871  ressprdsds  20874  prdsxmslem2  21032  zcld  21318  xrge0tsms  21339  metdsf  21352  metdsge  21353  minveclem1  21839  minveclem3b  21843  minveclem6  21849  uniioombllem4  21995  uniioombllem6  21997  ismbf3d  22061  i1f1lem  22096  reldv  22274  ellimc2  22281  limcflf  22285  limciun  22298  dvfval  22301  dvrec  22358  dvlipcn  22395  mdegle0  22477  ply1nzb  22523  quotlem  22696  taylfval  22754  ulmdvlem1  22795  ulmdvlem2  22796  ulmdvlem3  22797  psercn  22821  sqff1o  23456  lgsquadlem2  23630  cusgrasizeindslem2  24474  disjxwwlks  24736  wwlknfi  24738  disjxwwlkn  24745  grpoidval  25218  grpoidinv2  25220  grpoinv  25229  minvecolem1  25790  minvecolem5  25797  minvecolem6  25798  adjbdln  27002  rmoeq  27386  dfcnv2  27517  rexdiv  27622  xrge0tsmsd  27775  esumnul  28059  esum0  28060  hasheuni  28091  measvuni  28185  measdivcstOLD  28195  ddemeas  28208  eulerpartlemgs2  28319  probfinmeasbOLD  28367  0rrv  28390  signsplypnf  28507  signsply0  28508  subfacf  28619  subfacp1lem6  28629  cvmsss2  28719  cvmliftlem1  28730  fin2so  30040  supaddc  30041  supadd  30042  ptrest  30048  cnambfre  30063  dvtanlem  30064  upixp  30220  0totbnd  30269  prdsbnd  30289  prdstotbnd  30290  cntotbnd  30292  rrnequiv  30331  ac6s6  30580  0dioph  30712  vdioph  30713  rmxyelqirr  30846  pw2f1ocnv  30979  phisum  31159  limcdm0  31624  0cnf  31679  dvsinax  31708  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnprodlem3  31745  mbf0  31756  iblempty  31764  fourierdlem89  31978  fourierdlem91  31980  fourierdlem100  31989  fourierdlem108  31997  fourierdlem112  32001  eliunxp2  32923  bnj226  33789  bnj98  33925  bnj517  33943  bnj893  33986  bnj1137  34051  bj-rabtr  34497  cdlemefrs32fva  36126  cdlemkid5  36661  cdlemk56  36697  dihf11lem  36993  pwinfi  37749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618
This theorem depends on definitions:  df-bi 185  df-ral 2812
  Copyright terms: Public domain W3C validator