Theorem rgen 2783

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

Syntax hints:   -> wi 4   e. wcel 1867   A.wral 2773

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

This theorem depends on definitions:  df-bi 188  df-ral 2778

This theorem is referenced by:  rgenw  2784  mprg  2786  mprgbir  2787  r19.21be  2794  rgen2  2848  rgen2a  2850  rgen2aOLD  2851  nrex  2878  rexlimi  2905  rexlimiv  2909  sbcth2  3380  reuss  3751  r19.2zb  3884  ral0  3899  unimax  4248  mpteq1  4498  mpteq2ia  4500  reusv2lem4  4621  wfisg  5426  fnopab  5712  fmpti  6052  sorpssuni  6586  sorpssint  6587  onssmin  6630  tfis  6687  omssnlim  6712  finds  6725  finds2  6727  opabex3  6778  wfr3  7056  seqomlem2  7168  findcard3  7812  fifo  7944  fisupcl  7983  dfom3  8150  cantnfvalf  8167  rankf  8262  scottex  8353  cplem1  8357  harcard  8409  cardiun  8413  r0weon  8440  acnnum  8479  alephon  8496  alephsmo  8529  alephf1ALT  8530  alephfplem4  8534  dfac5lem4  8553  dfacacn  8567  kmlem1  8576  cflem  8672  cflecard  8679  cfsmolem  8696  fin23lem17  8764  hsmexlem4  8855  omina  9112  0tsk  9176  inar1  9196  wfgru  9237  reclem2pr  9469  nnssre  10609  dfnn2  10618  dfnn3  10619  nnind  10623  nnsub  10644  dfuzi  11022  uzinfmiOLD  11235  uzsupss  11252  cnref1o  11293  xrsupsslem  11588  xrinfmsslem  11589  xrsup0  11605  reltre  11626  rpltrp  11627  reltxrnmnf  11628  ser0f  12259  bccl  12500  hashkf  12510  hashbc  12607  wrdind  12814  sqrlem5  13289  rexuz3  13390  sqrtf  13405  ackbijnn  13864  incexclem  13872  prodf1f  13926  eff2  14131  reeff1  14152  sqrt2irr  14279  prmind2  14613  3prm  14619  pockthi  14829  infpn2  14835  prminf  14837  prmreclem2  14839  prmrec  14844  1arith  14849  1arith2  14850  vdwlem13  14921  ramz  14961  prmgap  15007  prmgaplcmOLD  15008  prmgaplcm  15009  prmgapprmo  15011  prmgapprmorOLD  15012  prmlem1a  15056  xpsff1o  15452  isacs1i  15541  dmaf  15922  cdaf  15923  coapm  15944  lublecllem  16212  pmtrdifel  17099  pmtrdifwrdel  17104  odf  17164  odfOLD  17180  efgrelexlemb  17378  dprd2da  17653  mgpf  17770  prdscrngd  17819  cnfld1  18971  cnsubglem  18995  cnmsubglem  19008  nn0srg  19014  rge0srg  19015  pmatcoe1fsupp  19702  isbasis3g  19941  basdif0  19945  distop  19988  mretopd  20085  2ndcsep  20451  refref  20505  kqf  20739  fbssfi  20829  filcon  20875  prdstmdd  21115  ustfilxp  21204  prdsxmslem2  21521  qdensere  21767  recld2  21809  ovolf  22412  dyadmax  22533  dveflem  22908  mdegxrf  22994  fta1  23238  vieta1  23242  aalioulem2  23266  taylfval  23291  pilem2  23384  pilem2OLD  23385  pilem3  23386  pilem3OLD  23387  recosf1o  23461  divlogrlim  23557  logcn  23569  ressatans  23837  leibpi  23845  ftalem3  23976  chtub  24117  2sqlem6  24274  2sqlem10  24279  chtppilim  24290  pntpbnd1  24401  pntlem3  24424  padicabvf  24446  axcontlem2  24972  isgrpoi  25902  cnid  26055  mulid  26060  cnrngo  26107  isvci  26177  isnvi  26208  ipasslem8  26454  hilid  26790  hlimf  26866  shsspwh  26875  pjrni  27331  pjmf1  27345  df0op2  27381  dfiop2  27382  hoaddcomi  27401  hoaddassi  27405  hocadddiri  27408  hocsubdiri  27409  hoaddid1i  27415  ho0coi  27417  hoid1i  27418  hoid1ri  27419  honegsubi  27425  hoddii  27618  lnopunilem2  27640  elunop2  27642  lnophm  27648  imaelshi  27687  cnlnadjlem8  27703  pjnmopi  27777  pjsdii  27784  pjddii  27785  pjtoi  27808  chirred  28024  nnindf  28369  nn0min  28371  esum2d  28903  dmvlsiga  28940  volmeas  29043  ddemeas  29048  sxbrsigalem3  29083  coinfliprv  29304  ballotlem7  29357  ballotlem7OLD  29395  signsw0glem  29431  bnj580  29713  bnj1384  29830  bnj1497  29858  kur14lem9  29926  msrf  30169  dfon2lem7  30423  frinsg  30471  bdayfo  30550  nodense  30564  fobigcup  30653  nn0prpwlem  30964  topmeet  31006  onsucsuccmpi  31089  taupilemrplb  31667  relowlssretop  31701  ptrecube  31848  poimirlem27  31875  heicant  31883  mblfinlem1  31885  volsupnfl  31893  dvtan  31900  itg2addnc  31904  indexa  31968  sstotbnd2  32014  heiborlem7  32057  atpsubN  33231  idldil  33592  cdleme50ldil  34028  mzpclall  35482  dgraaf  35925  dgraafOLD  35926  phisum  35990  arearect  36014  areaquad  36015  prmunb2  36511  radcnvrat  36515  upbdrech  37347  fsumiunss  37444  resincncf  37539  stoweidlem57  37705  wallispilem3  37716  stirlinglem13  37735  dirkertrigeqlem3  37749  fourierdlem62  37819  gsumge0cl  37968  tgoldbach  38531  2zlidl  38996  2zrngagrp  39005  2zrngnmlid  39011  crhmsubc  39142  drhmsubc  39144  drngcat  39145  fldcat  39146  fldhmsubc  39148  crhmsubcALTV  39161  drhmsubcALTV  39163  drngcatALTV  39164  fldcatALTV  39165  fldhmsubcALTV  39167  zlmodzxznm  39354  ldepsnlinc  39365  nn0sumshdiglem2  39498