Theorem rgen 2922

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

Syntax hints:   -> wi 4   e. wcel 1990   A.wral 2912

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

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  ralel  2923  rgenw  2924  mprg  2926  mprgbir  2927  r19.21be  2933  rgen2  2975  rgen2a  2977  nrex  3000  rexlimi  3024  rexlimiv  3027  sbcth2  3523  r19.2zb  4061  ral0  4076  unimax  4473  mpteq1  4737  mpteq2ia  4740  reusv2lem4  4872  wfisg  5715  fnopab  6018  fmpti  6383  sorpssuni  6946  sorpssint  6947  onssmin  6997  tfis  7054  omssnlim  7079  finds  7092  finds2  7094  opabex3  7146  wfr3  7435  seqomlem2  7546  findcard3  8203  fifo  8338  fisupcl  8375  dfom3  8544  cantnfvalf  8562  rankf  8657  scottex  8748  cplem1  8752  harcard  8804  cardiun  8808  r0weon  8835  acnnum  8875  alephon  8892  alephsmo  8925  alephf1ALT  8926  alephfplem4  8930  dfac5lem4  8949  dfacacn  8963  kmlem1  8972  cflem  9068  cflecard  9075  cfsmolem  9092  fin23lem17  9160  hsmexlem4  9251  omina  9513  0tsk  9577  inar1  9597  wfgru  9638  reclem2pr  9870  nnssre  11024  dfnn2  11033  dfnn3  11034  nnind  11038  nnsub  11059  dfuzi  11468  uzsupss  11780  cnref1o  11827  xrsupsslem  12137  xrinfmsslem  12138  xrsup0  12153  reltre  12170  rpltrp  12171  reltxrnmnf  12172  ser0f  12854  bccl  13109  hashkf  13119  hashbc  13237  wrdind  13476  sqrlem5  13987  rexuz3  14088  sqrtf  14103  ackbijnn  14560  incexclem  14568  prodf1f  14624  eff2  14829  reeff1  14850  sqrt2irr  14979  prmind2  15398  3prm  15406  phisum  15495  pockthi  15611  infpn2  15617  prminf  15619  prmreclem2  15621  prmrec  15626  1arith  15631  1arith2  15632  vdwlem13  15697  ramz  15729  prmgap  15763  prmgaplcm  15764  prmgapprmo  15766  prmlem1a  15813  xpsff1o  16228  isacs1i  16318  dmaf  16699  cdaf  16700  coapm  16721  lublecllem  16988  pmtrdifel  17900  pmtrdifwrdel  17905  odf  17956  efgrelexlemb  18163  dprd2da  18441  mgpf  18559  prdscrngd  18613  cnfld1  19771  cnsubglem  19795  cnmsubglem  19809  nn0srg  19816  rge0srg  19817  pmatcoe1fsupp  20506  isbasis3g  20753  basdif0  20757  distop  20799  mretopd  20896  2ndcsep  21262  refref  21316  kqf  21550  fbssfi  21641  filconn  21687  prdstmdd  21927  ustfilxp  22016  prdsxmslem2  22334  qdensere  22573  recld2  22617  isclmi0  22898  iscvsi  22929  ovolf  23250  dyadmax  23366  dveflem  23742  mdegxrf  23828  fta1  24063  vieta1  24067  aalioulem2  24088  taylfval  24113  pilem2  24206  pilem3  24207  recosf1o  24281  divlogrlim  24381  logcn  24393  ressatans  24661  leibpi  24669  ftalem3  24801  chtub  24937  2sqlem6  25148  2sqlem10  25153  chtppilim  25164  pntpbnd1  25275  pntlem3  25298  padicabvf  25320  axcontlem2  25845  nbgrnself  26257  vtxdginducedm1  26439  isgrpoi  27352  isvciOLD  27435  cnidOLD  27437  isnvi  27468  ipasslem8  27692  hilid  28018  hlimf  28094  shsspwh  28103  pjrni  28561  pjmf1  28575  df0op2  28611  dfiop2  28612  hoaddcomi  28631  hoaddassi  28635  hocadddiri  28638  hocsubdiri  28639  hoaddid1i  28645  ho0coi  28647  hoid1i  28648  hoid1ri  28649  honegsubi  28655  hoddii  28848  lnopunilem2  28870  elunop2  28872  lnophm  28878  imaelshi  28917  cnlnadjlem8  28933  pjnmopi  29007  pjsdii  29014  pjddii  29015  pjtoi  29038  chirred  29254  nnindf  29565  nn0min  29567  esum2d  30155  dmvlsiga  30192  volmeas  30294  ddemeas  30299  sxbrsigalem3  30334  coinfliprv  30544  ballotlem7  30597  signsw0glem  30630  rpsqrtcn  30671  tgoldbachgt  30741  bnj580  30983  bnj1384  31100  bnj1497  31128  kur14lem9  31196  msrf  31439  dfon2lem7  31694  frinsg  31742  bdayfo  31828  nodense  31842  fobigcup  32007  nn0prpwlem  32317  topmeet  32359  onsucsuccmpi  32442  taupilemrplb  33166  relowlssretop  33211  ptrecube  33409  poimirlem27  33436  heicant  33444  mblfinlem1  33446  volsupnfl  33454  dvtan  33460  itg2addnc  33464  indexa  33528  sstotbnd2  33573  heiborlem7  33616  atpsubN  35039  idldil  35400  cdleme50ldil  35836  mzpclall  37290  dgraaf  37717  arearect  37801  areaquad  37802  clsk1indlem2  38340  clsk1indlem4  38342  prmunb2  38510  radcnvrat  38513  unirnmapsn  39406  ssmapsn  39408  upbdrech  39519  supminfxr  39694  supminfxr2  39699  supminfxrrnmpt  39701  fsumiunss  39807  resincncf  40088  dmvolss  40202  volioof  40204  stoweidlem57  40274  wallispilem3  40284  stirlinglem13  40303  dirkertrigeqlem3  40317  fourierdlem62  40385  salexct  40552  salexct3  40560  salgencntex  40561  salgensscntex  40562  gsumge0cl  40588  0ome  40743  icoresmbl  40757  hoidmv1le  40808  smflimlem1  40979  smfpimbor1lem2  41006  smfliminflem  41036  fmtno4prm  41487  31prm  41512  tgoldbach  41705  tgoldbachOLD  41712  2zlidl  41934  2zrngagrp  41943  2zrngnmlid  41949  crhmsubc  42078  drhmsubc  42080  drngcat  42081  fldcat  42082  fldhmsubc  42084  crhmsubcALTV  42096  drhmsubcALTV  42098  drngcatALTV  42099  fldcatALTV  42100  fldhmsubcALTV  42102  zlmodzxznm  42286  ldepsnlinc  42297  nn0sumshdiglem2  42416  onsetrec  42451