Theorem rgenw 2781

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 2779	1 |- A. x e. A ph

Syntax hints:   e. wcel 1761   A.wral 2713

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

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

This theorem is referenced by:  rgen2w  2782  reuun1  3629  riinrab  4243  0disj  4282  iinexg  4449  epse  4699  xpiindi  4971  eliunxp  4973  opeliunxp2  4974  elrnmpti  5086  fnmpti  5536  eqfnfv  5794  eufnfv  5948  mpt2eq12  6145  porpss  6363  iunex  6556  mpt2ex  6649  suppssov1  6720  suppssfv  6724  onnseq  6801  ixpssmap  7293  boxcutc  7302  nneneq  7490  finsschain  7614  dfom3  7849  cantnfdm  7866  cantnfdmOLD  7868  cantnfOLD  7919  rankuni2b  8056  rankval4  8070  alephf1  8251  dfac4  8288  dfacacn  8306  infmap2  8383  cfeq0  8421  fin23lem28  8505  axdc2lem  8613  axcclem  8622  ac6  8645  iundom  8702  konigthlem  8728  iunctb  8734  tskmid  9003  supmul1  10291  supmullem2  10293  supmul  10294  uzf  10860  seqof  11859  hashbclem  12201  wrdexg  12240  rlimclim1  13019  fsumcom2  13237  ackbijnn  13287  sumhash  13954  ramcl  14086  prdsval  14389  prdsbas  14391  prdshom  14401  imasplusg  14451  imasmulr  14452  imasvsca  14454  imasip  14455  imasaddfnlem  14462  imasvscafn  14471  isfunc  14770  wunfunc  14805  isnat  14853  natffn  14855  wunnat  14862  fucsect  14878  setcepi  14952  dfod2  16058  ghmcyg  16365  gsum2d2lem  16455  gsum2d2  16456  gsumcom2  16457  dmdprd  16470  dprdval  16475  dprdvalOLD  16477  dprdf11  16503  dprdf11OLD  16510  dprd2d2  16533  dpjeq  16548  dpjeqOLD  16555  pgpfac1lem2  16566  pgpfac1lem3  16568  pgpfac1lem4  16569  00lsp  17040  ocv0  18061  frlmip  18162  ofco2  18291  tgidm  18544  pptbas  18571  tgrest  18722  iscnp2  18802  ist1-3  18912  discmp  18960  1stcfb  19008  lly1stc  19059  disllycmp  19061  dis1stc  19062  txbas  19099  ptbasfi  19113  ptpjopn  19144  dfac14  19150  ptrescn  19171  xkoptsub  19186  fclsval  19540  ptcmplem2  19584  ptcmplem3  19585  cnextrel  19594  tsmsfbas  19657  ustuqtop  19780  prdsxmetlem  19902  ressprdsds  19905  prdsxmslem2  20063  zcld  20349  xrge0tsms  20370  metdsf  20383  metdsge  20384  rrxip  20853  minveclem1  20870  minveclem3b  20874  minveclem6  20880  uniioombllem4  21025  uniioombllem6  21027  ismbf3d  21091  i1f1lem  21126  reldv  21304  ellimc2  21311  limcflf  21315  limciun  21328  dvfval  21331  dvrec  21388  dvlipcn  21425  mdegle0  21507  ply1nzb  21553  quotlem  21725  taylfval  21783  ulmdvlem1  21824  ulmdvlem2  21825  ulmdvlem3  21826  psercn  21850  sqff1o  22479  lgsquadlem2  22653  cusgrasizeindslem2  23317  grpoidval  23638  grpoidinv2  23640  grpoinv  23649  minvecolem1  24210  minvecolem5  24217  minvecolem6  24218  adjbdln  25422  rmoeq  25806  dfcnv2  25929  rexdiv  26034  xrge0tsmsd  26188  esumnul  26438  esum0  26439  hasheuni  26470  measvuni  26564  measdivcstOLD  26574  ddemeas  26588  eulerpartlemgs2  26693  probfinmeasbOLD  26741  0rrv  26764  signsplypnf  26881  signsply0  26882  signstlen  26898  subfacf  26993  subfacp1lem6  27003  cvmsss2  27093  cvmliftlem1  27104  fprodcom2  27424  fin2so  28341  supaddc  28342  supadd  28343  ptrest  28350  cnambfre  28365  dvtanlem  28366  comppfsc  28504  upixp  28548  0totbnd  28597  prdsbnd  28617  prdstotbnd  28618  cntotbnd  28620  rrnequiv  28659  ac6s6  28909  0dioph  29042  vdioph  29043  rmxyelqirr  29176  pw2f1ocnv  29311  phisum  29492  disjxwwlks  30293  wwlknfi  30295  disjxwwlkn  30489  eliunxp2  30645  bnj226  31559  bnj98  31694  bnj517  31712  bnj893  31755  bnj1137  31820  bj-rabtr  32165  cdlemefrs32fva  33766  cdlemkid5  34301  cdlemk56  34337  dihf11lem  34633