Theorem rgen 2771

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

Syntax hints:   -> wi 4   e. wcel 1755   A.wral 2705

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

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

This theorem is referenced by:  rgen2a  2772  rgenw  2773  mprg  2775  mprgbir  2776  rgen2  2802  r19.21be  2807  nrex  2808  rexlimi  2824  sbcth2  3269  reuss  3619  r19.2zb  3758  ral0  3772  unimax  4115  mpteq1  4360  mpteq2ia  4362  reusv2lem4  4484  fnopab  5523  fmpti  5854  sorpssuni  6358  sorpssint  6359  onssmin  6397  tfis  6454  omssnlim  6479  finds  6491  finds2  6493  opabex3  6545  seqomlem2  6892  findcard3  7543  fifo  7670  fisupcl  7705  dfom3  7841  cantnfvalf  7861  rankf  7989  scottex  8080  cplem1  8084  harcard  8136  cardiun  8140  r0weon  8167  acnnum  8210  alephon  8227  alephsmo  8260  alephf1ALT  8261  alephfplem4  8265  dfac5lem4  8284  dfacacn  8298  kmlem1  8307  cflem  8403  cflecard  8410  cfsmolem  8427  fin23lem17  8495  hsmexlem4  8586  omina  8845  0tsk  8909  inar1  8929  wfgru  8970  reclem2pr  9204  nnssre  10313  dfnn2  10322  dfnn3  10323  nnind  10327  nnsub  10347  dfuzi  10719  uzinfmi  10921  uzsupss  10934  cnref1o  10973  xrsupsslem  11256  xrinfmsslem  11257  xrsup0  11273  ser0f  11842  bccl  12081  hashkf  12088  hashbc  12189  wrdind  12354  sqrlem5  12719  rexuz3  12819  sqrf  12834  ackbijnn  13273  incexclem  13281  eff2  13365  reeff1  13386  sqr2irr  13513  prmind2  13756  3prm  13762  pockthi  13950  infpn2  13956  prminf  13958  prmreclem2  13960  prmrec  13965  1arith  13970  1arith2  13971  vdwlem13  14036  ramz  14068  prmlem1a  14116  xpsff1o  14488  isacs1i  14577  dmaf  14899  cdaf  14900  coapm  14921  lublecllem  15140  pmtrdifel  15965  pmtrdifwrdel  15970  odf  16019  efgrelexlemb  16226  dprd2da  16514  mgpf  16591  prdscrngd  16639  cnfld1  17684  cnsubglem  17705  cnmsubglem  17718  isbasis3g  18395  basdif0  18399  distop  18441  mretopd  18537  2ndcsep  18904  kqf  19161  fbssfi  19251  filcon  19297  prdstmdd  19535  ustfilxp  19628  prdsxmslem2  19945  qdensere  20190  recld2  20232  ehlbase  20751  ovolf  20806  dyadmax  20919  dveflem  21292  mdegxrf  21423  fta1  21658  vieta1  21662  aalioulem2  21683  taylfval  21708  pilem2  21801  pilem3  21802  recosf1o  21875  divlogrlim  21964  logcn  21976  ressatans  22213  leibpi  22221  ftalem3  22296  chtub  22435  2sqlem6  22592  2sqlem10  22597  chtppilim  22608  pntpbnd1  22719  pntlem3  22742  padicabvf  22764  axcontlem2  23033  isgrpoi  23507  cnid  23660  mulid  23665  cnrngo  23712  isvci  23782  isnvi  23813  ipasslem8  24059  hilid  24385  hlimf  24462  shsspwh  24471  pjrni  24927  pjmf1  24941  df0op2  24978  dfiop2  24979  hoaddcomi  24998  hoaddassi  25002  hocadddiri  25005  hocsubdiri  25006  hoaddid1i  25012  ho0coi  25014  hoid1i  25015  hoid1ri  25016  honegsubi  25022  hoddii  25215  lnopunilem2  25237  elunop2  25239  lnophm  25245  imaelshi  25284  cnlnadjlem8  25300  pjnmopi  25374  pjsdii  25381  pjddii  25382  pjtoi  25405  chirred  25621  nnindf  25911  nn0min  25912  nn0srg  26062  rge0srg  26063  rearchi  26163  cnzh  26252  rezh  26253  dmvlsiga  26425  volmeas  26500  ddemeas  26505  sxbrsigalem3  26540  coinfliprv  26712  ballotlem7  26765  signsw0glem  26801  signsvvf  26827  kur14lem9  26949  prodf1f  27253  dfon2lem7  27448  epsetlike  27501  wfisg  27516  frinsg  27552  wfr3  27588  tfrALTlem  27589  bdayfo  27662  nodense  27676  fobigcup  27777  onsucsuccmpi  28136  heicant  28267  mblfinlem1  28269  volsupnfl  28277  dvtan  28283  itg2addnc  28287  nn0prpwlem  28358  refref  28398  topmeet  28426  indexa  28468  sstotbnd2  28514  heiborlem7  28557  mzpclall  28905  dgraaf  29346  phisum  29409  arearect  29433  areaquad  29434  stoweidlem57  29695  wallispilem3  29705  stirlinglem13  29724  wwlktovf  30094  zlmodzxznm  30745  ldepsnlinc  30756  bnj580  31605  bnj1384  31722  bnj1497  31750  atpsubN  32967  idldil  33328  cdleme50ldil  33762  taupilemrplb  35184