Theorem rgenw 2818

Description: Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
rgenw.1	|- ph

Assertion

Ref	Expression
rgenw	|- A. x e. A ph

Proof of Theorem rgenw

Step	Hyp	Ref	Expression
1		rgenw.1	. . 3 |- ph
2	1	a1i 11	. 2 |- ( x e. A -> ph )
3	2	rgen 2817	1 |- A. x e. A ph

Syntax hints:   e. wcel 1819   A.wral 2807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619

This theorem depends on definitions:  df-bi 185  df-ral 2812

This theorem is referenced by:  rgen2w  2819  reuun1  3787  riinrab  4408  0disj  4449  iinexg  4616  epse  4871  xpiindi  5148  eliunxp  5150  opeliunxp2  5151  elrnmpti  5263  fnmpti  5715  eqfnfv  5982  eufnfv  6147  mpt2eq12  6356  porpss  6583  iunex  6779  mpt2ex  6876  suppssov1  6950  suppssfv  6954  onnseq  7033  ixpssmap  7522  boxcutc  7531  nneneq  7719  finsschain  7845  dfom3  8081  cantnfdm  8098  cantnfdmOLD  8100  cantnfOLD  8151  rankuni2b  8288  rankval4  8302  alephf1  8483  dfac4  8520  dfacacn  8538  infmap2  8615  cfeq0  8653  fin23lem28  8737  axdc2lem  8845  axcclem  8854  ac6  8877  iundom  8934  konigthlem  8960  iunctb  8966  tskmid  9235  supmul1  10528  supmullem2  10530  supmul  10531  uzf  11109  seqof  12166  hashbclem  12504  wrdexg  12563  rlimclim1  13379  fsumcom2  13600  ackbijnn  13651  fprodcom2  13799  sumhash  14426  ramcl  14558  prdsval  14871  prdsbas  14873  prdshom  14883  imasplusg  14933  imasmulr  14934  imasvsca  14936  imasip  14937  imasaddfnlem  14944  imasvscafn  14953  isfunc  15279  wunfunc  15314  isnat  15362  natffn  15364  wunnat  15371  fucsect  15387  setcepi  15493  dfod2  16712  ghmcyg  17024  gsum2d2lem  17127  gsum2d2  17128  gsumcom2  17129  dmdprd  17155  dprdval  17160  dprdvalOLD  17162  dprdf11  17189  dprdf11OLD  17196  dprd2d2  17219  dpjeq  17234  dpjeqOLD  17241  pgpfac1lem2  17252  pgpfac1lem3  17254  pgpfac1lem4  17255  mptscmfsupp0  17702  00lsp  17753  ocv0  18834  ofco2  19079  tgidm  19608  pptbas  19635  tgrest  19786  iscnp2  19866  ist1-3  19976  discmp  20024  1stcfb  20071  lly1stc  20122  disllycmp  20124  dis1stc  20125  comppfsc  20158  txbas  20193  ptbasfi  20207  ptpjopn  20238  dfac14  20244  ptrescn  20265  xkoptsub  20280  fclsval  20634  ptcmplem2  20678  ptcmplem3  20679  cnextrel  20688  tsmsfbas  20751  ustuqtop  20874  prdsxmetlem  20996  ressprdsds  20999  prdsxmslem2  21157  zcld  21443  xrge0tsms  21464  metdsf  21477  metdsge  21478  minveclem1  21964  minveclem3b  21968  minveclem6  21974  uniioombllem4  22120  uniioombllem6  22122  ismbf3d  22186  i1f1lem  22221  reldv  22399  ellimc2  22406  limcflf  22410  limciun  22423  dvfval  22426  dvrec  22483  dvlipcn  22520  mdegle0  22602  ply1nzb  22648  quotlem  22821  taylfval  22879  ulmdvlem1  22920  ulmdvlem2  22921  ulmdvlem3  22922  psercn  22946  sqff1o  23581  lgsquadlem2  23755  cusgrasizeindslem2  24600  disjxwwlks  24862  wwlknfi  24864  disjxwwlkn  24871  grpoidval  25344  grpoidinv2  25346  grpoinv  25355  minvecolem1  25916  minvecolem5  25923  minvecolem6  25924  adjbdln  27128  rmoeq  27512  mptexgf  27609  dfcnv2  27665  rexdiv  27774  xrge0tsmsd  27928  esumnul  28214  esum0  28215  hasheuni  28247  esum2d  28253  measvuni  28346  measdivcstOLD  28356  ddemeas  28369  eulerpartlemgs2  28494  probfinmeasbOLD  28542  0rrv  28565  signsplypnf  28682  signsply0  28683  subfacf  28794  subfacp1lem6  28804  cvmsss2  28894  cvmliftlem1  28905  fin2so  30202  supaddc  30203  supadd  30204  ptrest  30210  cnambfre  30225  dvtanlem  30226  upixp  30382  0totbnd  30431  prdsbnd  30451  prdstotbnd  30452  cntotbnd  30454  rrnequiv  30493  ac6s6  30742  0dioph  30874  vdioph  30875  rmxyelqirr  31008  pw2f1ocnv  31141  phisum  31321  limcdm0  31785  0cnf  31840  dvsinax  31869  ioodvbdlimc1lem2  31890  ioodvbdlimc2lem  31892  dvnprodlem3  31906  mbf0  31917  iblempty  31925  fourierdlem89  32139  fourierdlem91  32141  fourierdlem100  32150  fourierdlem108  32158  fourierdlem112  32162  eliunxp2  33025  bnj226  33890  bnj98  34026  bnj517  34044  bnj893  34087  bnj1137  34152  bj-rabtr  34598  cdlemefrs32fva  36227  cdlemkid5  36762  cdlemk56  36798  dihf11lem  37094  pwinfi  37850