Theorem rgen 2899

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 2804	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		rgen.1	. 2 |- ( x e. A -> ph )
3	1, 2	mpgbir 1596	1 |- A. x e. A ph

Syntax hints:   -> wi 4   e. wcel 1758   A.wral 2799

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

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

This theorem is referenced by:  rgen2a  2900  rgenw  2901  mprg  2903  mprgbir  2904  rgen2  2918  r19.21be  2923  nrex  2924  rexlimi  2940  sbcth2  3389  reuss  3742  r19.2zb  3881  ral0  3895  unimax  4238  mpteq1  4483  mpteq2ia  4485  reusv2lem4  4607  fnopab  5646  fmpti  5978  sorpssuni  6482  sorpssint  6483  onssmin  6521  tfis  6578  omssnlim  6603  finds  6615  finds2  6617  opabex3  6669  seqomlem2  7019  findcard3  7669  fifo  7796  fisupcl  7831  dfom3  7967  cantnfvalf  7987  rankf  8115  scottex  8206  cplem1  8210  harcard  8262  cardiun  8266  r0weon  8293  acnnum  8336  alephon  8353  alephsmo  8386  alephf1ALT  8387  alephfplem4  8391  dfac5lem4  8410  dfacacn  8424  kmlem1  8433  cflem  8529  cflecard  8536  cfsmolem  8553  fin23lem17  8621  hsmexlem4  8712  omina  8972  0tsk  9036  inar1  9056  wfgru  9097  reclem2pr  9331  nnssre  10440  dfnn2  10449  dfnn3  10450  nnind  10454  nnsub  10474  dfuzi  10846  uzinfmi  11048  uzsupss  11061  cnref1o  11100  xrsupsslem  11383  xrinfmsslem  11384  xrsup0  11400  ser0f  11979  bccl  12218  hashkf  12225  hashbc  12327  wrdind  12492  sqrlem5  12857  rexuz3  12957  sqrf  12972  ackbijnn  13412  incexclem  13420  eff2  13504  reeff1  13525  sqr2irr  13652  prmind2  13895  3prm  13901  pockthi  14089  infpn2  14095  prminf  14097  prmreclem2  14099  prmrec  14104  1arith  14109  1arith2  14110  vdwlem13  14175  ramz  14207  prmlem1a  14255  xpsff1o  14628  isacs1i  14717  dmaf  15039  cdaf  15040  coapm  15061  lublecllem  15280  pmtrdifel  16108  pmtrdifwrdel  16113  odf  16164  efgrelexlemb  16371  dprd2da  16666  mgpf  16782  prdscrngd  16831  cnfld1  17969  cnsubglem  17990  cnmsubglem  18003  nn0srg  18009  rge0srg  18010  isbasis3g  18689  basdif0  18693  distop  18735  mretopd  18831  2ndcsep  19198  kqf  19455  fbssfi  19545  filcon  19591  prdstmdd  19829  ustfilxp  19922  prdsxmslem2  20239  qdensere  20484  recld2  20526  ehlbase  21045  ovolf  21100  dyadmax  21214  dveflem  21587  mdegxrf  21675  fta1  21910  vieta1  21914  aalioulem2  21935  taylfval  21960  pilem2  22053  pilem3  22054  recosf1o  22127  divlogrlim  22216  logcn  22228  ressatans  22465  leibpi  22473  ftalem3  22548  chtub  22687  2sqlem6  22844  2sqlem10  22849  chtppilim  22860  pntpbnd1  22971  pntlem3  22994  padicabvf  23016  axcontlem2  23383  isgrpoi  23857  cnid  24010  mulid  24015  cnrngo  24062  isvci  24132  isnvi  24163  ipasslem8  24409  hilid  24735  hlimf  24812  shsspwh  24821  pjrni  25277  pjmf1  25291  df0op2  25328  dfiop2  25329  hoaddcomi  25348  hoaddassi  25352  hocadddiri  25355  hocsubdiri  25356  hoaddid1i  25362  ho0coi  25364  hoid1i  25365  hoid1ri  25366  honegsubi  25372  hoddii  25565  lnopunilem2  25587  elunop2  25589  lnophm  25595  imaelshi  25634  cnlnadjlem8  25650  pjnmopi  25724  pjsdii  25731  pjddii  25732  pjtoi  25755  chirred  25971  nnindf  26254  nn0min  26255  rearchi  26475  cnzh  26564  rezh  26565  dmvlsiga  26737  volmeas  26811  ddemeas  26816  sxbrsigalem3  26851  coinfliprv  27029  ballotlem7  27082  signsw0glem  27118  signsvvf  27144  kur14lem9  27266  prodf1f  27571  dfon2lem7  27766  epsetlike  27819  wfisg  27834  frinsg  27870  wfr3  27906  tfrALTlem  27907  bdayfo  27980  nodense  27994  fobigcup  28095  onsucsuccmpi  28453  heicant  28594  mblfinlem1  28596  volsupnfl  28604  dvtan  28610  itg2addnc  28614  nn0prpwlem  28685  refref  28725  topmeet  28753  indexa  28795  sstotbnd2  28841  heiborlem7  28884  mzpclall  29231  dgraaf  29672  phisum  29735  arearect  29759  areaquad  29760  stoweidlem57  30020  wallispilem3  30030  stirlinglem13  30049  wwlktovf  30419  zlmodzxznm  31191  ldepsnlinc  31202  pmatcoe1fsupp  31212  bnj580  32258  bnj1384  32375  bnj1497  32403  atpsubN  33755  idldil  34116  cdleme50ldil  34550  taupilemrplb  35972