Theorem rgenw 2825

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

Syntax hints:   e. wcel 1767   A.wral 2814

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

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

This theorem is referenced by:  rgen2w  2826  reuun1  3780  riinrab  4401  0disj  4440  iinexg  4607  epse  4862  xpiindi  5138  eliunxp  5140  opeliunxp2  5141  elrnmpti  5253  fnmpti  5709  eqfnfv  5976  eufnfv  6135  mpt2eq12  6342  porpss  6569  iunex  6765  mpt2ex  6861  suppssov1  6933  suppssfv  6937  onnseq  7016  ixpssmap  7504  boxcutc  7513  nneneq  7701  finsschain  7828  dfom3  8065  cantnfdm  8082  cantnfdmOLD  8084  cantnfOLD  8135  rankuni2b  8272  rankval4  8286  alephf1  8467  dfac4  8504  dfacacn  8522  infmap2  8599  cfeq0  8637  fin23lem28  8721  axdc2lem  8829  axcclem  8838  ac6  8861  iundom  8918  konigthlem  8944  iunctb  8950  tskmid  9219  supmul1  10509  supmullem2  10511  supmul  10512  uzf  11086  seqof  12133  hashbclem  12468  wrdexg  12524  rlimclim1  13334  fsumcom2  13555  ackbijnn  13606  sumhash  14277  ramcl  14409  prdsval  14713  prdsbas  14715  prdshom  14725  imasplusg  14775  imasmulr  14776  imasvsca  14778  imasip  14779  imasaddfnlem  14786  imasvscafn  14795  isfunc  15094  wunfunc  15129  isnat  15177  natffn  15179  wunnat  15186  fucsect  15202  setcepi  15276  dfod2  16401  ghmcyg  16713  gsum2d2lem  16816  gsum2d2  16817  gsumcom2  16818  dmdprd  16844  dprdval  16849  dprdvalOLD  16851  dprdf11  16877  dprdf11OLD  16884  dprd2d2  16907  dpjeq  16922  dpjeqOLD  16929  pgpfac1lem2  16940  pgpfac1lem3  16942  pgpfac1lem4  16943  mptscmfsupp0  17388  00lsp  17439  ocv0  18515  frlmip  18616  ofco2  18760  tgidm  19288  pptbas  19315  tgrest  19466  iscnp2  19546  ist1-3  19656  discmp  19704  1stcfb  19752  lly1stc  19803  disllycmp  19805  dis1stc  19806  comppfsc  19860  txbas  19895  ptbasfi  19909  ptpjopn  19940  dfac14  19946  ptrescn  19967  xkoptsub  19982  fclsval  20336  ptcmplem2  20380  ptcmplem3  20381  cnextrel  20390  tsmsfbas  20453  ustuqtop  20576  prdsxmetlem  20698  ressprdsds  20701  prdsxmslem2  20859  zcld  21145  xrge0tsms  21166  metdsf  21179  metdsge  21180  rrxip  21649  minveclem1  21666  minveclem3b  21670  minveclem6  21676  uniioombllem4  21822  uniioombllem6  21824  ismbf3d  21888  i1f1lem  21923  reldv  22101  ellimc2  22108  limcflf  22112  limciun  22125  dvfval  22128  dvrec  22185  dvlipcn  22222  mdegle0  22304  ply1nzb  22350  quotlem  22522  taylfval  22580  ulmdvlem1  22621  ulmdvlem2  22622  ulmdvlem3  22623  psercn  22647  efabl  22762  sqff1o  23281  lgsquadlem2  23455  cusgrasizeindslem2  24247  disjxwwlks  24509  wwlknfi  24511  disjxwwlkn  24518  grpoidval  24991  grpoidinv2  24993  grpoinv  25002  minvecolem1  25563  minvecolem5  25570  minvecolem6  25571  adjbdln  26775  rmoeq  27159  dfcnv2  27286  rexdiv  27387  xrge0tsmsd  27535  esumnul  27810  esum0  27811  hasheuni  27842  measvuni  27936  measdivcstOLD  27946  ddemeas  27959  eulerpartlemgs2  28070  probfinmeasbOLD  28118  0rrv  28141  signsplypnf  28258  signsply0  28259  signstlen  28275  subfacf  28370  subfacp1lem6  28380  cvmsss2  28470  cvmliftlem1  28481  fprodcom2  28967  fin2so  29893  supaddc  29894  supadd  29895  ptrest  29901  cnambfre  29916  dvtanlem  29917  upixp  30050  0totbnd  30099  prdsbnd  30119  prdstotbnd  30120  cntotbnd  30122  rrnequiv  30161  ac6s6  30411  0dioph  30543  vdioph  30544  rmxyelqirr  30677  pw2f1ocnv  30810  phisum  30991  limcdm0  31387  dvsinax  31468  ioodvbdlimc1lem2  31489  ioodvbdlimc2lem  31491  iblempty  31510  fourierdlem70  31704  fourierdlem80  31714  fourierdlem89  31723  fourierdlem91  31725  fourierdlem100  31734  fourierdlem108  31742  fourierdlem112  31746  eliunxp2  32218  bnj226  33086  bnj98  33221  bnj517  33239  bnj893  33282  bnj1137  33347  bj-rabtr  33795  cdlemefrs32fva  35413  cdlemkid5  35948  cdlemk56  35984  dihf11lem  36280