Theorem rgenw 2924

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

Syntax hints:   e. wcel 1990   A.wral 2912

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

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  rgen2w  2925  reuss  3908  reuun1  3909  rabnc  3962  riinrab  4596  0disj  4645  iinexg  4824  epse  5097  xpiindi  5257  eliunxp  5259  opeliunxp2  5260  elrnmpti  5376  cnviin  5672  fnmpti  6022  eqfnfv  6311  mptexgf  6485  eufnfv  6491  mpt2eq12  6715  porpss  6941  iunex  7147  abrexex2  7148  mpt2ex  7247  suppssov1  7327  suppssfv  7331  opeliunxp2f  7336  onnseq  7441  ixpssmap  7942  boxcutc  7951  nneneq  8143  finsschain  8273  dfom3  8544  cantnfdm  8561  rankuni2b  8716  rankval4  8730  alephf1  8908  dfac4  8945  dfacacn  8963  infmap2  9040  cfeq0  9078  fin23lem28  9162  axdc2lem  9270  axcclem  9279  ac6  9302  iundom  9364  konigthlem  9390  iunctb  9396  tskmid  9662  supaddc  10990  supadd  10991  supmul1  10992  supmullem2  10994  supmul  10995  uzf  11690  seqof  12858  hashbclem  13236  wrdexg  13315  rlimclim1  14276  fsumcom2  14505  fsumcom2OLD  14506  ackbijnn  14560  fprodcom2  14714  fprodcom2OLD  14715  lcmf0  15347  phisum  15495  sumhash  15600  ramcl  15733  prdsval  16115  prdsbas  16117  prdshom  16127  imasplusg  16177  imasmulr  16178  imasvsca  16180  imasip  16181  imasaddfnlem  16188  imasvscafn  16197  isfunc  16524  wunfunc  16559  isnat  16607  natffn  16609  wunnat  16616  fucsect  16632  setcepi  16738  dfod2  17981  ghmcyg  18297  gsum2d2lem  18372  gsum2d2  18373  gsumcom2  18374  dmdprd  18397  dprdval  18402  dprdf11  18422  dprd2d2  18443  dpjeq  18458  pgpfac1lem2  18474  pgpfac1lem3  18476  pgpfac1lem4  18477  mptscmfsupp0  18928  00lsp  18981  ocv0  20021  ofco2  20257  tgidm  20784  pptbas  20812  tgrest  20963  iscnp2  21043  ist1-3  21153  discmp  21201  1stcfb  21248  lly1stc  21299  disllycmp  21301  dis1stc  21302  comppfsc  21335  txbas  21370  ptbasfi  21384  ptpjopn  21415  dfac14  21421  ptrescn  21442  xkoptsub  21457  fclsval  21812  ptcmplem2  21857  ptcmplem3  21858  cnextrel  21867  tsmsfbas  21931  ustuqtop  22050  prdsxmetlem  22173  ressprdsds  22176  prdsxmslem2  22334  zcld  22616  xrge0tsms  22637  metdsf  22651  metdsge  22652  minveclem1  23195  minveclem3b  23199  minveclem6  23205  uniioombllem4  23354  uniioombllem6  23356  ismbf3d  23421  i1f1lem  23456  reldv  23634  ellimc2  23641  limcflf  23645  limciun  23658  dvfval  23661  dvrec  23718  dvlipcn  23757  mdegle0  23837  ply1nzb  23882  quotlem  24055  taylfval  24113  ulmdvlem1  24154  ulmdvlem2  24155  ulmdvlem3  24156  psercn  24180  sqff1o  24908  lgsquadlem2  25106  disjxwwlksn  26799  wwlksnfi  26801  disjxwwlkn  26808  grpoidval  27367  grpoidinv2  27369  grpoinv  27379  minvecolem1  27730  minvecolem5  27737  minvecolem6  27738  adjbdln  28942  rmoeqALT  29327  dfcnv2  29476  rexdiv  29634  xrge0tsmsd  29785  esumnul  30110  esum0  30111  hasheuni  30147  esum2d  30155  ldgenpisyslem3  30228  measvuni  30277  measdivcstOLD  30287  ddemeas  30299  carsgclctunlem2  30381  eulerpartlemgs2  30442  probfinmeasbOLD  30490  0rrv  30513  signsplypnf  30627  signsply0  30628  hgt750lemb  30734  bnj226  30802  bnj98  30937  bnj517  30955  bnj893  30998  bnj1137  31063  subfacf  31157  subfacp1lem6  31167  cvmsss2  31256  cvmliftlem1  31267  nulssgt  31909  bj-rabtr  32926  bj-rabtrALTALT  32928  relowlssretop  33211  fin2so  33396  matunitlindflem1  33405  ptrest  33408  poimirlem23  33432  poimirlem24  33433  poimirlem27  33436  poimirlem30  33439  poimirlem32  33441  cnambfre  33458  upixp  33524  0totbnd  33572  prdsbnd  33592  prdstotbnd  33593  cntotbnd  33595  rrnequiv  33634  ac6s6  33980  cdlemefrs32fva  35688  cdlemkid5  36223  cdlemk56  36259  dihf11lem  36555  0dioph  37342  vdioph  37343  rmxyelqirr  37475  pw2f1ocnv  37604  pwinfi  37869  eliunov2  37971  fvmptiunrelexplb0d  37976  fvmptiunrelexplb1d  37978  iunrelexp0  37994  ntrrn  38420  dssmapntrcls  38426  wessf1ornlem  39371  axccdom  39416  mpteq1df  39443  fsumiunss  39807  limcdm0  39850  liminfval2  40000  liminflelimsuplem  40007  cnrefiisplem  40055  0cnf  40090  dvsinax  40127  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnprodlem3  40163  mbf0  40173  iblempty  40181  fourierdlem89  40412  fourierdlem91  40414  fourierdlem100  40423  fourierdlem108  40431  fourierdlem112  40435  salexct3  40560  salgensscntex  40562  omeiunle  40731  0ome  40743  hoissrrn  40763  ovn0  40780  hoissrrn2  40792  hspmbl  40843  ovolval5lem2  40867  ovolval5lem3  40868  iunhoiioolem  40889  vonioolem2  40895  vonicclem2  40898  smflimlem1  40979  smfsuplem1  41017  smfinflem  41023  smflimsuplem1  41026  smflimsuplem2  41027  smflimsuplem3  41028  smflimsuplem4  41029  smflimsuplem5  41030  smflimsuplem7  41032  smfliminflem  41036  iccelpart  41369  eliunxp2  42112