Theorem rgenw 2804

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

Syntax hints:   e. wcel 1756   A.wral 2736

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

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

This theorem is referenced by:  rgen2w  2805  reuun1  3653  riinrab  4267  0disj  4306  iinexg  4473  epse  4724  xpiindi  4996  eliunxp  4998  opeliunxp2  4999  elrnmpti  5111  fnmpti  5560  eqfnfv  5818  eufnfv  5972  mpt2eq12  6167  porpss  6385  iunex  6578  mpt2ex  6671  suppssov1  6742  suppssfv  6746  onnseq  6826  ixpssmap  7318  boxcutc  7327  nneneq  7515  finsschain  7639  dfom3  7874  cantnfdm  7891  cantnfdmOLD  7893  cantnfOLD  7944  rankuni2b  8081  rankval4  8095  alephf1  8276  dfac4  8313  dfacacn  8331  infmap2  8408  cfeq0  8446  fin23lem28  8530  axdc2lem  8638  axcclem  8647  ac6  8670  iundom  8727  konigthlem  8753  iunctb  8759  tskmid  9028  supmul1  10316  supmullem2  10318  supmul  10319  uzf  10885  seqof  11884  hashbclem  12226  wrdexg  12265  rlimclim1  13044  fsumcom2  13262  ackbijnn  13312  sumhash  13979  ramcl  14111  prdsval  14414  prdsbas  14416  prdshom  14426  imasplusg  14476  imasmulr  14477  imasvsca  14479  imasip  14480  imasaddfnlem  14487  imasvscafn  14496  isfunc  14795  wunfunc  14830  isnat  14878  natffn  14880  wunnat  14887  fucsect  14903  setcepi  14977  dfod2  16086  ghmcyg  16393  gsum2d2lem  16487  gsum2d2  16488  gsumcom2  16489  dmdprd  16502  dprdval  16507  dprdvalOLD  16509  dprdf11  16535  dprdf11OLD  16542  dprd2d2  16565  dpjeq  16580  dpjeqOLD  16587  pgpfac1lem2  16598  pgpfac1lem3  16600  pgpfac1lem4  16601  mptscmfsupp0  17033  00lsp  17084  ocv0  18124  frlmip  18225  ofco2  18354  tgidm  18607  pptbas  18634  tgrest  18785  iscnp2  18865  ist1-3  18975  discmp  19023  1stcfb  19071  lly1stc  19122  disllycmp  19124  dis1stc  19125  txbas  19162  ptbasfi  19176  ptpjopn  19207  dfac14  19213  ptrescn  19234  xkoptsub  19249  fclsval  19603  ptcmplem2  19647  ptcmplem3  19648  cnextrel  19657  tsmsfbas  19720  ustuqtop  19843  prdsxmetlem  19965  ressprdsds  19968  prdsxmslem2  20126  zcld  20412  xrge0tsms  20433  metdsf  20446  metdsge  20447  rrxip  20916  minveclem1  20933  minveclem3b  20937  minveclem6  20943  uniioombllem4  21088  uniioombllem6  21090  ismbf3d  21154  i1f1lem  21189  reldv  21367  ellimc2  21374  limcflf  21378  limciun  21391  dvfval  21394  dvrec  21451  dvlipcn  21488  mdegle0  21570  ply1nzb  21616  quotlem  21788  taylfval  21846  ulmdvlem1  21887  ulmdvlem2  21888  ulmdvlem3  21889  psercn  21913  sqff1o  22542  lgsquadlem2  22716  cusgrasizeindslem2  23404  grpoidval  23725  grpoidinv2  23727  grpoinv  23736  minvecolem1  24297  minvecolem5  24304  minvecolem6  24305  adjbdln  25509  rmoeq  25893  dfcnv2  26016  rexdiv  26123  xrge0tsmsd  26275  esumnul  26524  esum0  26525  hasheuni  26556  measvuni  26650  measdivcstOLD  26660  ddemeas  26674  eulerpartlemgs2  26785  probfinmeasbOLD  26833  0rrv  26856  signsplypnf  26973  signsply0  26974  signstlen  26990  subfacf  27085  subfacp1lem6  27095  cvmsss2  27185  cvmliftlem1  27196  fprodcom2  27517  fin2so  28442  supaddc  28443  supadd  28444  ptrest  28451  cnambfre  28466  dvtanlem  28467  comppfsc  28605  upixp  28649  0totbnd  28698  prdsbnd  28718  prdstotbnd  28719  cntotbnd  28721  rrnequiv  28760  ac6s6  29010  0dioph  29143  vdioph  29144  rmxyelqirr  29277  pw2f1ocnv  29412  phisum  29593  disjxwwlks  30394  wwlknfi  30396  disjxwwlkn  30590  eliunxp2  30747  bnj226  31821  bnj98  31956  bnj517  31974  bnj893  32017  bnj1137  32082  bj-rabtr  32528  cdlemefrs32fva  34140  cdlemkid5  34675  cdlemk56  34711  dihf11lem  35007