Theorem rgen 2776

Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)

Hypothesis

Ref	Expression
rgen.1	|- ( x e. A -> ph )

Assertion

Ref	Expression
rgen	|- A. x e. A ph

Proof of Theorem rgen

Step	Hyp	Ref	Expression
1		df-ral 2715	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		rgen.1	. 2 |- ( x e. A -> ph )
3	1, 2	mpgbir 1595	1 |- A. x e. A ph

Syntax hints:   -> wi 4   e. wcel 1756   A.wral 2710

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 2715

This theorem is referenced by:  rgen2a  2777  rgenw  2778  mprg  2780  mprgbir  2781  rgen2  2807  r19.21be  2812  nrex  2813  rexlimi  2829  sbcth2  3276  reuss  3626  r19.2zb  3765  ral0  3779  unimax  4122  mpteq1  4367  mpteq2ia  4369  reusv2lem4  4491  fnopab  5530  fmpti  5861  sorpssuni  6364  sorpssint  6365  onssmin  6403  tfis  6460  omssnlim  6485  finds  6497  finds2  6499  opabex3  6551  seqomlem2  6898  findcard3  7547  fifo  7674  fisupcl  7709  dfom3  7845  cantnfvalf  7865  rankf  7993  scottex  8084  cplem1  8088  harcard  8140  cardiun  8144  r0weon  8171  acnnum  8214  alephon  8231  alephsmo  8264  alephf1ALT  8265  alephfplem4  8269  dfac5lem4  8288  dfacacn  8302  kmlem1  8311  cflem  8407  cflecard  8414  cfsmolem  8431  fin23lem17  8499  hsmexlem4  8590  omina  8850  0tsk  8914  inar1  8934  wfgru  8975  reclem2pr  9209  nnssre  10318  dfnn2  10327  dfnn3  10328  nnind  10332  nnsub  10352  dfuzi  10724  uzinfmi  10926  uzsupss  10939  cnref1o  10978  xrsupsslem  11261  xrinfmsslem  11262  xrsup0  11278  ser0f  11851  bccl  12090  hashkf  12097  hashbc  12198  wrdind  12363  sqrlem5  12728  rexuz3  12828  sqrf  12843  ackbijnn  13283  incexclem  13291  eff2  13375  reeff1  13396  sqr2irr  13523  prmind2  13766  3prm  13772  pockthi  13960  infpn2  13966  prminf  13968  prmreclem2  13970  prmrec  13975  1arith  13980  1arith2  13981  vdwlem13  14046  ramz  14078  prmlem1a  14126  xpsff1o  14498  isacs1i  14587  dmaf  14909  cdaf  14910  coapm  14931  lublecllem  15150  pmtrdifel  15977  pmtrdifwrdel  15982  odf  16031  efgrelexlemb  16238  dprd2da  16529  mgpf  16644  prdscrngd  16693  cnfld1  17816  cnsubglem  17837  cnmsubglem  17850  nn0srg  17856  rge0srg  17857  isbasis3g  18529  basdif0  18533  distop  18575  mretopd  18671  2ndcsep  19038  kqf  19295  fbssfi  19385  filcon  19431  prdstmdd  19669  ustfilxp  19762  prdsxmslem2  20079  qdensere  20324  recld2  20366  ehlbase  20885  ovolf  20940  dyadmax  21053  dveflem  21426  mdegxrf  21514  fta1  21749  vieta1  21753  aalioulem2  21774  taylfval  21799  pilem2  21892  pilem3  21893  recosf1o  21966  divlogrlim  22055  logcn  22067  ressatans  22304  leibpi  22312  ftalem3  22387  chtub  22526  2sqlem6  22683  2sqlem10  22688  chtppilim  22699  pntpbnd1  22810  pntlem3  22833  padicabvf  22855  axcontlem2  23162  isgrpoi  23636  cnid  23789  mulid  23794  cnrngo  23841  isvci  23911  isnvi  23942  ipasslem8  24188  hilid  24514  hlimf  24591  shsspwh  24600  pjrni  25056  pjmf1  25070  df0op2  25107  dfiop2  25108  hoaddcomi  25127  hoaddassi  25131  hocadddiri  25134  hocsubdiri  25135  hoaddid1i  25141  ho0coi  25143  hoid1i  25144  hoid1ri  25145  honegsubi  25151  hoddii  25344  lnopunilem2  25366  elunop2  25368  lnophm  25374  imaelshi  25413  cnlnadjlem8  25429  pjnmopi  25503  pjsdii  25510  pjddii  25511  pjtoi  25534  chirred  25750  nnindf  26040  nn0min  26041  rearchi  26262  cnzh  26351  rezh  26352  dmvlsiga  26524  volmeas  26599  ddemeas  26604  sxbrsigalem3  26639  coinfliprv  26817  ballotlem7  26870  signsw0glem  26906  signsvvf  26932  kur14lem9  27054  prodf1f  27358  dfon2lem7  27553  epsetlike  27606  wfisg  27621  frinsg  27657  wfr3  27693  tfrALTlem  27694  bdayfo  27767  nodense  27781  fobigcup  27882  onsucsuccmpi  28241  heicant  28379  mblfinlem1  28381  volsupnfl  28389  dvtan  28395  itg2addnc  28399  nn0prpwlem  28470  refref  28510  topmeet  28538  indexa  28580  sstotbnd2  28626  heiborlem7  28669  mzpclall  29016  dgraaf  29457  phisum  29520  arearect  29544  areaquad  29545  stoweidlem57  29805  wallispilem3  29815  stirlinglem13  29834  wwlktovf  30204  pmatcollpw2lem  30820  zlmodzxznm  30928  ldepsnlinc  30939  bnj580  31793  bnj1384  31910  bnj1497  31938  atpsubN  33237  idldil  33598  cdleme50ldil  34032  taupilemrplb  35454