Theorem rgenw 2765

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

Syntax hints:   e. wcel 1842   A.wral 2754

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

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

This theorem is referenced by:  rgen2w  2766  reuun1  3732  riinrab  4347  0disj  4388  iinexg  4554  epse  4806  xpiindi  4959  eliunxp  4961  opeliunxp2  4962  elrnmpti  5074  fnmpti  5692  eqfnfv  5959  eufnfv  6127  mpt2eq12  6338  porpss  6566  iunex  6764  mpt2ex  6861  suppssov1  6935  suppssfv  6939  onnseq  7048  ixpssmap  7541  boxcutc  7550  nneneq  7738  finsschain  7861  dfom3  8097  cantnfdm  8113  cantnfdmOLD  8115  cantnfOLD  8166  rankuni2b  8303  rankval4  8317  alephf1  8498  dfac4  8535  dfacacn  8553  infmap2  8630  cfeq0  8668  fin23lem28  8752  axdc2lem  8860  axcclem  8869  ac6  8892  iundom  8949  konigthlem  8975  iunctb  8981  tskmid  9248  supmul1  10548  supmullem2  10550  supmul  10551  uzf  11130  seqof  12208  hashbclem  12550  wrdexg  12609  rlimclim1  13517  fsumcom2  13740  ackbijnn  13791  fprodcom2  13940  sumhash  14624  ramcl  14756  prdsval  15069  prdsbas  15071  prdshom  15081  imasplusg  15131  imasmulr  15132  imasvsca  15134  imasip  15135  imasaddfnlem  15142  imasvscafn  15151  isfunc  15477  wunfunc  15512  isnat  15560  natffn  15562  wunnat  15569  fucsect  15585  setcepi  15691  dfod2  16910  ghmcyg  17222  gsum2d2lem  17322  gsum2d2  17323  gsumcom2  17324  dmdprd  17349  dprdval  17354  dprdvalOLD  17356  dprdf11  17383  dprdf11OLD  17390  dprd2d2  17413  dpjeq  17428  dpjeqOLD  17435  pgpfac1lem2  17446  pgpfac1lem3  17448  pgpfac1lem4  17449  mptscmfsupp0  17896  00lsp  17947  ocv0  19006  ofco2  19245  tgidm  19774  pptbas  19801  tgrest  19953  iscnp2  20033  ist1-3  20143  discmp  20191  1stcfb  20238  lly1stc  20289  disllycmp  20291  dis1stc  20292  comppfsc  20325  txbas  20360  ptbasfi  20374  ptpjopn  20405  dfac14  20411  ptrescn  20432  xkoptsub  20447  fclsval  20801  ptcmplem2  20845  ptcmplem3  20846  cnextrel  20855  tsmsfbas  20918  ustuqtop  21041  prdsxmetlem  21163  ressprdsds  21166  prdsxmslem2  21324  zcld  21610  xrge0tsms  21631  metdsf  21644  metdsge  21645  minveclem1  22131  minveclem3b  22135  minveclem6  22141  uniioombllem4  22287  uniioombllem6  22289  ismbf3d  22353  i1f1lem  22388  reldv  22566  ellimc2  22573  limcflf  22577  limciun  22590  dvfval  22593  dvrec  22650  dvlipcn  22687  mdegle0  22769  ply1nzb  22815  quotlem  22988  taylfval  23046  ulmdvlem1  23087  ulmdvlem2  23088  ulmdvlem3  23089  psercn  23113  sqff1o  23837  lgsquadlem2  24011  cusgrasizeindslem2  24891  disjxwwlks  25153  wwlknfi  25155  disjxwwlkn  25162  grpoidval  25632  grpoidinv2  25634  grpoinv  25643  minvecolem1  26204  minvecolem5  26211  minvecolem6  26212  adjbdln  27415  rmoeq  27801  mptexgf  27908  dfcnv2  27961  rexdiv  28074  xrge0tsmsd  28228  esumnul  28495  esum0  28496  hasheuni  28532  esum2d  28540  ldgenpisyslem3  28613  measvuni  28662  measdivcstOLD  28672  ddemeas  28685  carsgclctunlem2  28767  eulerpartlemgs2  28825  probfinmeasbOLD  28873  0rrv  28896  signsplypnf  29013  signsply0  29014  bnj226  29116  bnj98  29252  bnj517  29270  bnj893  29313  bnj1137  29378  subfacf  29472  subfacp1lem6  29482  cvmsss2  29571  cvmliftlem1  29582  bj-rabtr  31062  relowlssretop  31280  fin2so  31412  supaddc  31413  supadd  31414  ptrest  31420  cnambfre  31435  dvtanlemOLD  31437  upixp  31502  0totbnd  31551  prdsbnd  31571  prdstotbnd  31572  cntotbnd  31574  rrnequiv  31613  ac6s6  31862  cdlemefrs32fva  33419  cdlemkid5  33954  cdlemk56  33990  dihf11lem  34286  0dioph  35073  vdioph  35074  rmxyelqirr  35207  pw2f1ocnv  35341  phisum  35523  pwinfi  35615  eliunov2  35658  fvmptiunrelexplb0d  35663  fvmptiunrelexplb1d  35665  iunrelexp0  35681  limcdm0  36992  0cnf  37047  dvsinax  37076  ioodvbdlimc1lem2  37097  ioodvbdlimc2lem  37099  dvnprodlem3  37113  mbf0  37124  iblempty  37132  fourierdlem89  37346  fourierdlem91  37348  fourierdlem100  37357  fourierdlem108  37365  fourierdlem112  37369  iccelpart  37700  eliunxp2  38434