Theorem rgen 2803

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

Syntax hints:   -> wi 4   e. wcel 1804   A.wral 2793

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

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

This theorem is referenced by:  rgenw  2804  mprg  2806  mprgbir  2807  r19.21be  2814  rgen2  2868  rgen2a  2870  rgen2aOLD  2871  nrex  2898  rexlimi  2925  rexlimiv  2929  sbcth2  3408  reuss  3764  r19.2zb  3905  ral0  3919  unimax  4270  mpteq1  4517  mpteq2ia  4519  reusv2lem4  4641  fnopab  5695  fmpti  6039  sorpssuni  6574  sorpssint  6575  onssmin  6617  tfis  6674  omssnlim  6699  finds  6711  finds2  6713  opabex3  6764  seqomlem2  7118  findcard3  7765  fifo  7894  fisupcl  7930  dfom3  8067  cantnfvalf  8087  rankf  8215  scottex  8306  cplem1  8310  harcard  8362  cardiun  8366  r0weon  8393  acnnum  8436  alephon  8453  alephsmo  8486  alephf1ALT  8487  alephfplem4  8491  dfac5lem4  8510  dfacacn  8524  kmlem1  8533  cflem  8629  cflecard  8636  cfsmolem  8653  fin23lem17  8721  hsmexlem4  8812  omina  9072  0tsk  9136  inar1  9156  wfgru  9197  reclem2pr  9429  nnssre  10547  dfnn2  10556  dfnn3  10557  nnind  10561  nnsub  10581  dfuzi  10960  uzinfmi  11172  uzsupss  11185  cnref1o  11226  xrsupsslem  11509  xrinfmsslem  11510  xrsup0  11526  ser0f  12142  bccl  12382  hashkf  12389  hashbc  12484  wrdind  12684  sqrlem5  13062  rexuz3  13163  sqrtf  13178  ackbijnn  13622  incexclem  13630  prodf1f  13683  eff2  13816  reeff1  13837  sqrt2irr  13964  prmind2  14210  3prm  14216  pockthi  14407  infpn2  14413  prminf  14415  prmreclem2  14417  prmrec  14422  1arith  14427  1arith2  14428  vdwlem13  14493  ramz  14525  prmlem1a  14574  xpsff1o  14947  isacs1i  15036  dmaf  15355  cdaf  15356  coapm  15377  lublecllem  15597  pmtrdifel  16484  pmtrdifwrdel  16489  odf  16540  efgrelexlemb  16747  dprd2da  17070  mgpf  17189  prdscrngd  17241  cnfld1  18422  cnsubglem  18446  cnmsubglem  18459  nn0srg  18465  rge0srg  18466  pmatcoe1fsupp  19180  isbasis3g  19428  basdif0  19432  distop  19475  mretopd  19571  2ndcsep  19938  refref  19992  kqf  20226  fbssfi  20316  filcon  20362  prdstmdd  20600  ustfilxp  20693  prdsxmslem2  21010  qdensere  21255  recld2  21297  ovolf  21871  dyadmax  21985  dveflem  22358  mdegxrf  22446  fta1  22682  vieta1  22686  aalioulem2  22707  taylfval  22732  pilem2  22825  pilem3  22826  recosf1o  22900  divlogrlim  22994  logcn  23006  ressatans  23243  leibpi  23251  ftalem3  23326  chtub  23465  2sqlem6  23622  2sqlem10  23627  chtppilim  23638  pntpbnd1  23749  pntlem3  23772  padicabvf  23794  axcontlem2  24246  isgrpoi  25178  cnid  25331  mulid  25336  cnrngo  25383  isvci  25453  isnvi  25484  ipasslem8  25730  hilid  26056  hlimf  26133  shsspwh  26142  pjrni  26598  pjmf1  26612  df0op2  26649  dfiop2  26650  hoaddcomi  26669  hoaddassi  26673  hocadddiri  26676  hocsubdiri  26677  hoaddid1i  26683  ho0coi  26685  hoid1i  26686  hoid1ri  26687  honegsubi  26693  hoddii  26886  lnopunilem2  26908  elunop2  26910  lnophm  26916  imaelshi  26955  cnlnadjlem8  26971  pjnmopi  27045  pjsdii  27052  pjddii  27053  pjtoi  27076  chirred  27292  nnindf  27588  nn0min  27589  dmvlsiga  28107  volmeas  28181  ddemeas  28186  sxbrsigalem3  28221  coinfliprv  28399  ballotlem7  28452  signsw0glem  28488  kur14lem9  28636  msrf  28880  dfon2lem7  29197  epsetlike  29250  wfisg  29265  frinsg  29301  wfr3  29337  tfrALTlem  29338  bdayfo  29411  nodense  29425  fobigcup  29526  onsucsuccmpi  29884  heicant  30025  mblfinlem1  30027  volsupnfl  30035  dvtan  30041  itg2addnc  30045  nn0prpwlem  30116  topmeet  30158  indexa  30200  sstotbnd2  30246  heiborlem7  30289  mzpclall  30635  dgraaf  31072  phisum  31135  arearect  31159  areaquad  31160  prmunb2  31167  radcnvrat  31171  upbdrech  31459  resincncf  31631  stoweidlem57  31793  wallispilem3  31803  stirlinglem13  31822  dirkertrigeqlem3  31836  fourierdlem62  31905  etransc  32020  2zlidl  32567  2zrngagrp  32576  2zrngnmlid  32582  crhmsubc  32754  drhmsubc  32756  drngcat  32757  fldcat  32758  fldhmsubc  32760  crhmsubcOLD  32773  drhmsubcOLD  32775  drngcatOLD  32776  fldcatOLD  32777  fldhmsubcOLD  32779  zlmodzxznm  32968  ldepsnlinc  32979  bnj580  33839  bnj1384  33956  bnj1497  33984  atpsubN  35352  idldil  35713  cdleme50ldil  36149  taupilemrplb  37570