Theorem rgen 2763

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

Syntax hints:   -> wi 4   e. wcel 1842   A.wral 2753

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

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

This theorem is referenced by:  rgenw  2764  mprg  2766  mprgbir  2767  r19.21be  2774  rgen2  2828  rgen2a  2830  rgen2aOLD  2831  nrex  2858  rexlimi  2885  rexlimiv  2889  sbcth2  3360  reuss  3730  r19.2zb  3862  ral0  3877  unimax  4225  mpteq1  4474  mpteq2ia  4476  reusv2lem4  4597  wfisg  5401  fnopab  5687  fmpti  6031  sorpssuni  6570  sorpssint  6571  onssmin  6614  tfis  6671  omssnlim  6696  finds  6709  finds2  6711  opabex3  6762  wfr3  7040  seqomlem2  7152  findcard3  7796  fifo  7925  fisupcl  7960  dfom3  8096  cantnfvalf  8115  rankf  8243  scottex  8334  cplem1  8338  harcard  8390  cardiun  8394  r0weon  8421  acnnum  8464  alephon  8481  alephsmo  8514  alephf1ALT  8515  alephfplem4  8519  dfac5lem4  8538  dfacacn  8552  kmlem1  8561  cflem  8657  cflecard  8664  cfsmolem  8681  fin23lem17  8749  hsmexlem4  8840  omina  9098  0tsk  9162  inar1  9182  wfgru  9223  reclem2pr  9455  nnssre  10579  dfnn2  10588  dfnn3  10589  nnind  10593  nnsub  10614  dfuzi  10993  uzinfmi  11205  uzsupss  11218  cnref1o  11259  xrsupsslem  11550  xrinfmsslem  11551  xrsup0  11567  ser0f  12202  bccl  12442  hashkf  12452  hashbc  12549  wrdind  12756  sqrlem5  13227  rexuz3  13328  sqrtf  13343  ackbijnn  13789  incexclem  13797  prodf1f  13851  eff2  14041  reeff1  14062  sqrt2irr  14189  prmind2  14435  3prm  14441  pockthi  14632  infpn2  14638  prminf  14640  prmreclem2  14642  prmrec  14647  1arith  14652  1arith2  14653  vdwlem13  14718  ramz  14750  prmlem1a  14799  xpsff1o  15180  isacs1i  15269  dmaf  15650  cdaf  15651  coapm  15672  lublecllem  15940  pmtrdifel  16827  pmtrdifwrdel  16832  odf  16883  efgrelexlemb  17090  dprd2da  17409  mgpf  17528  prdscrngd  17580  cnfld1  18761  cnsubglem  18785  cnmsubglem  18798  nn0srg  18804  rge0srg  18805  pmatcoe1fsupp  19492  isbasis3g  19740  basdif0  19744  distop  19787  mretopd  19884  2ndcsep  20250  refref  20304  kqf  20538  fbssfi  20628  filcon  20674  prdstmdd  20912  ustfilxp  21005  prdsxmslem2  21322  qdensere  21567  recld2  21609  ovolf  22183  dyadmax  22297  dveflem  22670  mdegxrf  22758  fta1  22994  vieta1  22998  aalioulem2  23019  taylfval  23044  pilem2  23137  pilem3  23138  recosf1o  23212  divlogrlim  23308  logcn  23320  ressatans  23588  leibpi  23596  ftalem3  23727  chtub  23866  2sqlem6  24023  2sqlem10  24028  chtppilim  24039  pntpbnd1  24150  pntlem3  24173  padicabvf  24195  axcontlem2  24672  isgrpoi  25600  cnid  25753  mulid  25758  cnrngo  25805  isvci  25875  isnvi  25906  ipasslem8  26152  hilid  26478  hlimf  26555  shsspwh  26564  pjrni  27020  pjmf1  27034  df0op2  27070  dfiop2  27071  hoaddcomi  27090  hoaddassi  27094  hocadddiri  27097  hocsubdiri  27098  hoaddid1i  27104  ho0coi  27106  hoid1i  27107  hoid1ri  27108  honegsubi  27114  hoddii  27307  lnopunilem2  27329  elunop2  27331  lnophm  27337  imaelshi  27376  cnlnadjlem8  27392  pjnmopi  27466  pjsdii  27473  pjddii  27474  pjtoi  27497  chirred  27713  nnindf  28047  nn0min  28049  esum2d  28526  dmvlsiga  28563  volmeas  28666  ddemeas  28671  sxbrsigalem3  28706  coinfliprv  28913  ballotlem7  28966  signsw0glem  29002  bnj580  29285  bnj1384  29402  bnj1497  29430  kur14lem9  29498  msrf  29741  dfon2lem7  29995  frinsg  30043  bdayfo  30122  nodense  30136  fobigcup  30225  nn0prpwlem  30537  topmeet  30579  onsucsuccmpi  30662  taupilemrplb  31233  relowlssretop  31266  heicant  31401  mblfinlem1  31403  volsupnfl  31411  dvtan  31418  itg2addnc  31422  indexa  31486  sstotbnd2  31532  heiborlem7  31575  atpsubN  32750  idldil  33111  cdleme50ldil  33547  mzpclall  35001  dgraaf  35440  phisum  35503  arearect  35527  areaquad  35528  prmunb2  36019  radcnvrat  36023  upbdrech  36854  resincncf  37026  stoweidlem57  37188  wallispilem3  37198  stirlinglem13  37217  dirkertrigeqlem3  37231  fourierdlem62  37300  2zlidl  38232  2zrngagrp  38241  2zrngnmlid  38247  crhmsubc  38378  drhmsubc  38380  drngcat  38381  fldcat  38382  fldhmsubc  38384  crhmsubcALTV  38397  drhmsubcALTV  38399  drngcatALTV  38400  fldcatALTV  38401  fldhmsubcALTV  38403  zlmodzxznm  38590  ldepsnlinc  38601  nn0sumshdiglem2  38734