Theorem rgenw 2768

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

Syntax hints:   e. wcel 1904   A.wral 2756

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

This theorem depends on definitions:  df-bi 190  df-ral 2761

This theorem is referenced by:  rgen2w  2769  reuun1  3716  riinrab  4345  0disj  4388  iinexg  4561  epse  4822  xpiindi  4975  eliunxp  4977  opeliunxp2  4978  elrnmpti  5091  fnmpti  5716  eqfnfv  5991  eufnfv  6156  mpt2eq12  6370  porpss  6594  iunex  6792  mpt2ex  6889  suppssov1  6966  suppssfv  6970  opeliunxp2f  6975  onnseq  7081  ixpssmap  7574  boxcutc  7583  nneneq  7773  finsschain  7899  dfom3  8170  cantnfdm  8187  rankuni2b  8342  rankval4  8356  alephf1  8534  dfac4  8571  dfacacn  8589  infmap2  8666  cfeq0  8704  fin23lem28  8788  axdc2lem  8896  axcclem  8905  ac6  8928  iundom  8985  konigthlem  9011  iunctb  9017  tskmid  9283  supaddc  10596  supadd  10597  supmul1  10598  supmullem2  10600  supmul  10601  uzf  11185  seqof  12308  hashbclem  12656  wrdexg  12729  rlimclim1  13686  fsumcom2  13912  ackbijnn  13963  fprodcom2  14115  lcmf0  14686  sumhash  14920  ramcl  15066  prdsval  15431  prdsbas  15433  prdshom  15443  imasplusg  15496  imasmulr  15497  imasvsca  15499  imasip  15500  imasaddfnlem  15512  imasvscafn  15521  isfunc  15847  wunfunc  15882  isnat  15930  natffn  15932  wunnat  15939  fucsect  15955  setcepi  16061  dfod2  17293  ghmcyg  17608  gsum2d2lem  17683  gsum2d2  17684  gsumcom2  17685  dmdprd  17708  dprdval  17713  dprdf11  17734  dprd2d2  17755  dpjeq  17770  pgpfac1lem2  17786  pgpfac1lem3  17788  pgpfac1lem4  17789  mptscmfsupp0  18231  00lsp  18282  ocv0  19317  ofco2  19553  tgidm  20073  pptbas  20100  tgrest  20252  iscnp2  20332  ist1-3  20442  discmp  20490  1stcfb  20537  lly1stc  20588  disllycmp  20590  dis1stc  20591  comppfsc  20624  txbas  20659  ptbasfi  20673  ptpjopn  20704  dfac14  20710  ptrescn  20731  xkoptsub  20746  fclsval  21101  ptcmplem2  21146  ptcmplem3  21147  cnextrel  21156  tsmsfbas  21220  ustuqtop  21339  prdsxmetlem  21461  ressprdsds  21464  prdsxmslem2  21622  zcld  21909  xrge0tsms  21930  metdsf  21943  metdsge  21944  metdsfOLD  21958  metdsgeOLD  21959  minveclem1  22444  minveclem3b  22448  minveclem6  22454  minveclem3bOLD  22460  minveclem6OLD  22466  uniioombllem4  22623  uniioombllem6  22625  ismbf3d  22689  i1f1lem  22726  reldv  22904  ellimc2  22911  limcflf  22915  limciun  22928  dvfval  22931  dvrec  22988  dvlipcn  23025  mdegle0  23105  ply1nzb  23150  quotlem  23332  taylfval  23393  ulmdvlem1  23434  ulmdvlem2  23435  ulmdvlem3  23436  psercn  23460  sqff1o  24188  lgsquadlem2  24362  cusgrasizeindslem2  25281  disjxwwlks  25543  wwlknfi  25545  disjxwwlkn  25552  grpoidval  26025  grpoidinv2  26027  grpoinv  26036  minvecolem1  26597  minvecolem5  26604  minvecolem6  26605  minvecolem5OLD  26614  minvecolem6OLD  26615  adjbdln  27817  rmoeqALT  28202  mptexgf  28301  dfcnv2  28354  rexdiv  28470  xrge0tsmsd  28622  esumnul  28943  esum0  28944  hasheuni  28980  esum2d  28988  ldgenpisyslem3  29061  measvuni  29110  measdivcstOLD  29120  ddemeas  29132  carsgclctunlem2  29224  eulerpartlemgs2  29286  probfinmeasbOLD  29334  0rrv  29357  signsplypnf  29511  signsply0  29512  bnj226  29614  bnj98  29750  bnj517  29768  bnj893  29811  bnj1137  29876  subfacf  29970  subfacp1lem6  29980  cvmsss2  30069  cvmliftlem1  30080  bj-rabtr  31601  bj-rabtrALTALT  31603  relowlssretop  31836  fin2so  31996  ptrest  32003  poimirlem23  32027  poimirlem24  32028  poimirlem27  32031  poimirlem30  32034  poimirlem32  32036  cnambfre  32053  dvtanlemOLD  32055  upixp  32120  0totbnd  32169  prdsbnd  32189  prdstotbnd  32190  cntotbnd  32192  rrnequiv  32231  ac6s6  32479  cdlemefrs32fva  34038  cdlemkid5  34573  cdlemk56  34609  dihf11lem  34905  0dioph  35692  vdioph  35693  rmxyelqirr  35829  pw2f1ocnv  35963  phisum  36147  pwinfi  36239  eliunov2  36342  fvmptiunrelexplb0d  36347  fvmptiunrelexplb1d  36349  iunrelexp0  36365  wessf1ornlem  37530  fsumiunss  37750  limcdm0  37795  0cnf  37851  dvsinax  37880  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  dvnprodlem3  37920  mbf0  37931  iblempty  37939  fourierdlem89  38171  fourierdlem91  38173  fourierdlem100  38182  fourierdlem108  38190  fourierdlem112  38194  salexct3  38313  salgensscntex  38315  omeiunle  38457  0ome  38469  hoissrrn  38489  ovn0  38506  hoissrrn2  38518  hspmbl  38569  ovolval5lem2  38593  ovolval5lem3  38594  iccelpart  38892  eliunxp2  40623