Theorem rgenw 2733

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

Syntax hints:   e. wcel 1721   A.wral 2666

This theorem is referenced by:  rgen2w  2734  reuun1  3583  riinrab  4126  0disj  4165  iinexg  4320  epse  4525  xpiindi  4969  eliunxp  4971  opeliunxp2  4972  elrnmpti  5080  fnmpti  5532  eqfnfv  5786  eufnfv  5931  iunex  5950  mpt2eq12  6093  mpt2ex  6384  porpss  6485  onnseq  6565  ixpssmap  7055  boxcutc  7064  nneneq  7249  finsschain  7371  dfom3  7558  cantnfdm  7575  cantnf  7605  rankuni2b  7735  rankval4  7749  alephf1  7922  dfac4  7959  dfacacn  7977  infmap2  8054  cfeq0  8092  fin23lem28  8176  axdc2lem  8284  axcclem  8293  ac6  8316  iundom  8373  konigthlem  8399  iunctb  8405  tskmid  8671  supmul1  9929  supmullem2  9931  supmul  9932  uzf  10447  seqof  11335  hashbclem  11656  wrdexg  11694  rlimclim1  12294  fsumcom2  12513  ackbijnn  12562  sumhash  13220  ramcl  13352  prdsval  13633  prdsbas  13635  prdshom  13644  imasplusg  13698  imasmulr  13699  imasvsca  13701  imasaddfnlem  13708  imasvscafn  13717  isfunc  14016  wunfunc  14051  isnat  14099  natffn  14101  wunnat  14108  fucsect  14124  setcepi  14198  spwpr4c  14619  dfod2  15155  ghmcyg  15460  gsum2d2lem  15502  gsum2d2  15503  gsumcom2  15504  dmdprd  15514  dprdval  15516  dprdf11  15536  dprd2d2  15557  dpjeq  15572  pgpfac1lem2  15588  pgpfac1lem3  15590  pgpfac1lem4  15591  00lsp  16012  ocv0  16859  tgidm  17000  pptbas  17027  tgrest  17177  iscnp2  17257  ist1-3  17367  discmp  17415  1stcfb  17461  lly1stc  17512  disllycmp  17514  dis1stc  17515  txbas  17552  ptbasfi  17566  ptpjopn  17597  dfac14  17603  ptrescn  17624  xkoptsub  17639  fclsval  17993  ptcmplem2  18037  ptcmplem3  18038  cnextrel  18047  tsmsfbas  18110  ustuqtop  18229  prdsxmetlem  18351  ressprdsds  18354  prdsxmslem2  18512  zcld  18797  xrge0tsms  18818  metdsf  18831  metdsge  18832  minveclem1  19278  minveclem3b  19282  minveclem6  19288  uniioombllem4  19431  uniioombllem6  19433  ismbf3d  19499  i1f1lem  19534  reldv  19710  ellimc2  19717  limcflf  19721  limciun  19734  dvfval  19737  dvrec  19794  dvlipcn  19831  mdegle0  19953  ply1nzb  19998  quotlem  20170  taylfval  20228  ulmdvlem1  20269  ulmdvlem2  20270  ulmdvlem3  20271  psercn  20295  sqff1o  20918  lgsquadlem2  21092  cusgrasizeindslem2  21436  grpoidval  21757  grpoidinv2  21759  grpoinv  21768  minvecolem1  22329  minvecolem5  22336  minvecolem6  22337  adjbdln  23539  rexdiv  24125  xrge0tsmsd  24176  esumnul  24396  esum0  24397  hasheuni  24428  measvuni  24521  measdivcstOLD  24531  probfinmeasbOLD  24639  0rrv  24662  subfacf  24814  subfacp1lem6  24824  cvmsss2  24914  cvmliftlem1  24925  fprodcom2  25261  supaddc  26137  supadd  26138  cnambfre  26154  comppfsc  26277  upixp  26321  0totbnd  26372  prdsbnd  26392  prdstotbnd  26393  cntotbnd  26395  rrnequiv  26434  0dioph  26727  vdioph  26728  rmxyelqirr  26863  pw2f1ocnv  26998  phisum  27386  bnj226  28807  bnj98  28944  bnj517  28962  bnj893  29005  bnj1137  29070  cdlemefrs32fva  30882  cdlemkid5  31417  cdlemk56  31453  dihf11lem  31749

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

This theorem depends on definitions:  df-bi 178  df-ral 2671