Theorem rgen 2824

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

Syntax hints:   -> wi 4   e. wcel 1767   A.wral 2814

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

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

This theorem is referenced by:  rgenw  2825  mprg  2827  mprgbir  2828  r19.21be  2835  rgen2  2889  rgen2a  2891  rgen2aOLD  2892  nrex  2919  rexlimi  2945  rexlimiv  2949  sbcth2  3426  reuss  3779  r19.2zb  3918  ral0  3932  unimax  4281  mpteq1  4527  mpteq2ia  4529  reusv2lem4  4651  fnopab  5704  fmpti  6043  sorpssuni  6572  sorpssint  6573  onssmin  6611  tfis  6668  omssnlim  6693  finds  6705  finds2  6707  opabex3  6763  seqomlem2  7116  findcard3  7762  fifo  7891  fisupcl  7926  dfom3  8063  cantnfvalf  8083  rankf  8211  scottex  8302  cplem1  8306  harcard  8358  cardiun  8362  r0weon  8389  acnnum  8432  alephon  8449  alephsmo  8482  alephf1ALT  8483  alephfplem4  8487  dfac5lem4  8506  dfacacn  8520  kmlem1  8529  cflem  8625  cflecard  8632  cfsmolem  8649  fin23lem17  8717  hsmexlem4  8808  omina  9068  0tsk  9132  inar1  9152  wfgru  9193  reclem2pr  9425  nnssre  10539  dfnn2  10548  dfnn3  10549  nnind  10553  nnsub  10573  dfuzi  10950  uzinfmi  11160  uzsupss  11173  cnref1o  11214  xrsupsslem  11497  xrinfmsslem  11498  xrsup0  11514  ser0f  12127  bccl  12367  hashkf  12374  hashbc  12467  wrdind  12664  wwlktovf  12856  sqrlem5  13042  rexuz3  13143  sqrtf  13158  ackbijnn  13602  incexclem  13610  eff2  13694  reeff1  13715  sqrt2irr  13842  prmind2  14086  3prm  14092  pockthi  14283  infpn2  14289  prminf  14291  prmreclem2  14293  prmrec  14298  1arith  14303  1arith2  14304  vdwlem13  14369  ramz  14401  prmlem1a  14449  xpsff1o  14822  isacs1i  14911  dmaf  15233  cdaf  15234  coapm  15255  lublecllem  15474  pmtrdifel  16308  pmtrdifwrdel  16313  odf  16364  efgrelexlemb  16571  dprd2da  16890  mgpf  17006  prdscrngd  17058  cnfld1  18230  cnsubglem  18251  cnmsubglem  18264  nn0srg  18270  rge0srg  18271  pmatcoe1fsupp  18985  isbasis3g  19233  basdif0  19237  distop  19279  mretopd  19375  2ndcsep  19742  kqf  19999  fbssfi  20089  filcon  20135  prdstmdd  20373  ustfilxp  20466  prdsxmslem2  20783  qdensere  21028  recld2  21070  ehlbase  21589  ovolf  21644  dyadmax  21758  dveflem  22131  mdegxrf  22219  fta1  22454  vieta1  22458  aalioulem2  22479  taylfval  22504  pilem2  22597  pilem3  22598  recosf1o  22671  divlogrlim  22760  logcn  22772  ressatans  23009  leibpi  23017  ftalem3  23092  chtub  23231  2sqlem6  23388  2sqlem10  23393  chtppilim  23404  pntpbnd1  23515  pntlem3  23538  padicabvf  23560  axcontlem2  23960  isgrpoi  24892  cnid  25045  mulid  25050  cnrngo  25097  isvci  25167  isnvi  25198  ipasslem8  25444  hilid  25770  hlimf  25847  shsspwh  25856  pjrni  26312  pjmf1  26326  df0op2  26363  dfiop2  26364  hoaddcomi  26383  hoaddassi  26387  hocadddiri  26390  hocsubdiri  26391  hoaddid1i  26397  ho0coi  26399  hoid1i  26400  hoid1ri  26401  honegsubi  26407  hoddii  26600  lnopunilem2  26622  elunop2  26624  lnophm  26630  imaelshi  26669  cnlnadjlem8  26685  pjnmopi  26759  pjsdii  26766  pjddii  26767  pjtoi  26790  chirred  27006  nnindf  27294  nn0min  27295  rearchi  27511  cnzh  27603  rezh  27604  dmvlsiga  27785  volmeas  27859  ddemeas  27864  sxbrsigalem3  27899  coinfliprv  28077  ballotlem7  28130  signsw0glem  28166  signsvvf  28192  kur14lem9  28314  prodf1f  28619  dfon2lem7  28814  epsetlike  28867  wfisg  28882  frinsg  28918  wfr3  28954  tfrALTlem  28955  bdayfo  29028  nodense  29042  fobigcup  29143  onsucsuccmpi  29501  heicant  29642  mblfinlem1  29644  volsupnfl  29652  dvtan  29658  itg2addnc  29662  nn0prpwlem  29733  refref  29773  topmeet  29801  indexa  29843  sstotbnd2  29889  heiborlem7  29932  mzpclall  30279  dgraaf  30717  phisum  30780  arearect  30804  areaquad  30805  prmunb2  30810  upbdrech  31098  iooinlbub  31114  resincncf  31229  0cnf  31231  dvsinax  31257  dvcosax  31272  mbf0  31291  stoweidlem57  31373  wallispilem3  31383  stirlinglem13  31402  dirkertrigeqlem3  31416  fourierdlem43  31466  fourierdlem57  31480  fourierdlem58  31481  fourierdlem62  31485  fourierdlem103  31526  fourierdlem104  31527  fouriersw  31548  zlmodzxznm  32188  ldepsnlinc  32199  bnj580  33059  bnj1384  33176  bnj1497  33204  atpsubN  34558  idldil  34919  cdleme50ldil  35353  taupilemrplb  36775