Theorem rgenw 2721

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

Syntax hints:   e. wcel 1872   A.wral 2709

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

This theorem depends on definitions:  df-bi 188  df-ral 2714

This theorem is referenced by:  rgen2w  2722  reuun1  3693  riinrab  4313  0disj  4354  iinexg  4522  epse  4774  xpiindi  4927  eliunxp  4929  opeliunxp2  4930  elrnmpti  5042  fnmpti  5662  eqfnfv  5930  eufnfv  6093  mpt2eq12  6304  porpss  6528  iunex  6726  mpt2ex  6823  suppssov1  6897  suppssfv  6901  opeliunxp2f  6906  onnseq  7013  ixpssmap  7506  boxcutc  7515  nneneq  7703  finsschain  7829  dfom3  8100  cantnfdm  8116  rankuni2b  8271  rankval4  8285  alephf1  8462  dfac4  8499  dfacacn  8517  infmap2  8594  cfeq0  8632  fin23lem28  8716  axdc2lem  8824  axcclem  8833  ac6  8856  iundom  8913  konigthlem  8939  iunctb  8945  tskmid  9211  supaddc  10520  supadd  10521  supmul1  10522  supmullem2  10524  supmul  10525  uzf  11108  seqof  12215  hashbclem  12558  wrdexg  12625  rlimclim1  13547  fsumcom2  13773  ackbijnn  13824  fprodcom2  13976  lcmf0  14545  sumhash  14779  ramcl  14925  prdsval  15291  prdsbas  15293  prdshom  15303  imasplusg  15356  imasmulr  15357  imasvsca  15359  imasip  15360  imasaddfnlem  15372  imasvscafn  15381  isfunc  15707  wunfunc  15742  isnat  15790  natffn  15792  wunnat  15799  fucsect  15815  setcepi  15921  dfod2  17153  ghmcyg  17468  gsum2d2lem  17543  gsum2d2  17544  gsumcom2  17545  dmdprd  17568  dprdval  17573  dprdf11  17594  dprd2d2  17615  dpjeq  17630  pgpfac1lem2  17646  pgpfac1lem3  17648  pgpfac1lem4  17649  mptscmfsupp0  18091  00lsp  18142  ocv0  19177  ofco2  19413  tgidm  19933  pptbas  19960  tgrest  20112  iscnp2  20192  ist1-3  20302  discmp  20350  1stcfb  20397  lly1stc  20448  disllycmp  20450  dis1stc  20451  comppfsc  20484  txbas  20519  ptbasfi  20533  ptpjopn  20564  dfac14  20570  ptrescn  20591  xkoptsub  20606  fclsval  20960  ptcmplem2  21005  ptcmplem3  21006  cnextrel  21015  tsmsfbas  21079  ustuqtop  21198  prdsxmetlem  21320  ressprdsds  21323  prdsxmslem2  21481  zcld  21768  xrge0tsms  21789  metdsf  21802  metdsge  21803  metdsfOLD  21817  metdsgeOLD  21818  minveclem1  22303  minveclem3b  22307  minveclem6  22313  minveclem3bOLD  22319  minveclem6OLD  22325  uniioombllem4  22481  uniioombllem6  22483  ismbf3d  22547  i1f1lem  22584  reldv  22762  ellimc2  22769  limcflf  22773  limciun  22786  dvfval  22789  dvrec  22846  dvlipcn  22883  mdegle0  22963  ply1nzb  23008  quotlem  23190  taylfval  23251  ulmdvlem1  23292  ulmdvlem2  23293  ulmdvlem3  23294  psercn  23318  sqff1o  24046  lgsquadlem2  24220  cusgrasizeindslem2  25139  disjxwwlks  25401  wwlknfi  25403  disjxwwlkn  25410  grpoidval  25881  grpoidinv2  25883  grpoinv  25892  minvecolem1  26453  minvecolem5  26460  minvecolem6  26461  minvecolem5OLD  26470  minvecolem6OLD  26471  adjbdln  27673  rmoeqALT  28060  mptexgf  28166  dfcnv2  28220  rexdiv  28341  xrge0tsmsd  28495  esumnul  28816  esum0  28817  hasheuni  28853  esum2d  28861  ldgenpisyslem3  28934  measvuni  28983  measdivcstOLD  28993  ddemeas  29006  carsgclctunlem2  29098  eulerpartlemgs2  29160  probfinmeasbOLD  29208  0rrv  29231  signsplypnf  29386  signsply0  29387  bnj226  29489  bnj98  29625  bnj517  29643  bnj893  29686  bnj1137  29751  subfacf  29845  subfacp1lem6  29855  cvmsss2  29944  cvmliftlem1  29955  bj-rabtr  31444  bj-rabtrALTALT  31446  relowlssretop  31673  fin2so  31839  ptrest  31846  poimirlem23  31870  poimirlem24  31871  poimirlem27  31874  poimirlem30  31877  poimirlem32  31879  cnambfre  31896  dvtanlemOLD  31898  upixp  31963  0totbnd  32012  prdsbnd  32032  prdstotbnd  32033  cntotbnd  32035  rrnequiv  32074  ac6s6  32322  cdlemefrs32fva  33879  cdlemkid5  34414  cdlemk56  34450  dihf11lem  34746  0dioph  35533  vdioph  35534  rmxyelqirr  35671  pw2f1ocnv  35805  phisum  35989  pwinfi  36081  eliunov2  36184  fvmptiunrelexplb0d  36189  fvmptiunrelexplb1d  36191  iunrelexp0  36207  wessf1ornlem  37363  fsumiunss  37538  limcdm0  37581  0cnf  37637  dvsinax  37666  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  dvnprodlem3  37706  mbf0  37717  iblempty  37725  fourierdlem89  37942  fourierdlem91  37944  fourierdlem100  37953  fourierdlem108  37961  fourierdlem112  37965  omeiunle  38189  0ome  38201  hoissrrn  38218  ovn0  38235  hoissrrn2  38247  iccelpart  38560  eliunxp2  39708