Theorem rgen 2731

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

Syntax hints:   -> wi 4   e. wcel 1721   A.wral 2666

This theorem is referenced by:  rgen2a  2732  rgenw  2733  mprg  2735  mprgbir  2736  rgen2  2762  r19.21be  2767  nrex  2768  rexlimi  2783  sbcth2  3204  reuss  3582  r19.2zb  3678  ral0  3692  unimax  4009  mpteq1  4249  mpteq2ia  4251  reusv2lem4  4686  onssmin  4736  tfis  4793  omssnlim  4818  finds  4830  finds2  4832  fnopab  5528  fmpti  5851  opabex3  5949  sorpssuni  6490  sorpssint  6491  seqomlem2  6667  findcard3  7309  fifo  7395  fisupcl  7428  dfom3  7558  cantnfvalf  7576  rankf  7676  scottex  7765  cplem1  7769  harcard  7821  cardiun  7825  r0weon  7850  acnnum  7889  alephon  7906  alephsmo  7939  alephf1ALT  7940  alephfplem4  7944  dfac5lem4  7963  dfacacn  7977  kmlem1  7986  cflem  8082  cflecard  8089  cfsmolem  8106  fin23lem17  8174  hsmexlem4  8265  omina  8522  0tsk  8586  inar1  8606  wfgru  8647  reclem2pr  8881  nnssre  9960  dfnn2  9969  dfnn3  9970  nnind  9974  nnsub  9994  dfuzi  10316  uzinfmi  10511  uzsupss  10524  cnref1o  10563  xrsupsslem  10841  xrinfmsslem  10842  xrsup0  10858  ser0f  11331  bccl  11568  hashkf  11575  hashbc  11657  wrdind  11746  sqrlem5  12007  rexuz3  12107  sqrf  12122  ackbijnn  12562  incexclem  12571  eff2  12655  reeff1  12676  sqr2irr  12803  prmind2  13045  3prm  13051  pockthi  13230  infpn2  13236  prminf  13238  prmreclem2  13240  prmrec  13245  1arith  13250  1arith2  13251  vdwlem13  13316  ramz  13348  prmlem1a  13384  xpsff1o  13748  isacs1i  13837  dmaf  14159  cdaf  14160  coapm  14181  lubid  14394  odf  15130  efgrelexlemb  15337  dprd2da  15555  mgpf  15630  prdscrngd  15674  cnfld1  16681  cnsubglem  16702  cnmsubglem  16716  isbasis3g  16969  basdif0  16973  distop  17015  mretopd  17111  2ndcsep  17475  kqf  17732  fbssfi  17822  filcon  17868  prdstmdd  18106  ustfilxp  18195  prdsxmslem2  18512  qdensere  18757  recld2  18798  ovolf  19331  dyadmax  19443  dveflem  19816  mdegxrf  19944  fta1  20178  vieta1  20182  aalioulem2  20203  taylfval  20228  pilem2  20321  pilem3  20322  recosf1o  20390  divlogrlim  20479  logcn  20491  ressatans  20727  leibpi  20735  ftalem3  20810  chtub  20949  2sqlem6  21106  2sqlem10  21111  chtppilim  21122  pntpbnd1  21233  pntlem3  21256  padicabvf  21278  isgrpoi  21739  cnid  21892  mulid  21897  cnrngo  21944  isvci  22014  isnvi  22045  ipasslem8  22291  hilid  22616  hlimf  22693  shsspwh  22701  pjrni  23157  pjmf1  23171  df0op2  23208  dfiop2  23209  hoaddcomi  23228  hoaddassi  23232  hocadddiri  23235  hocsubdiri  23236  hoaddid1i  23242  ho0coi  23244  hoid1i  23245  hoid1ri  23246  honegsubi  23252  hoddii  23445  lnopunilem2  23467  elunop2  23469  lnophm  23475  imaelshi  23514  cnlnadjlem8  23530  pjnmopi  23604  pjsdii  23611  pjddii  23612  pjtoi  23635  chirred  23851  cnzh  24307  rezh  24308  dmvlsiga  24465  volmeas  24540  sxbrsigalem3  24575  coinfliprv  24693  ballotlem7  24746  kur14lem9  24853  prodf1f  25173  dfon2lem7  25359  epsetlike  25408  wfisg  25423  frinsg  25459  wfr3  25489  bdayfo  25543  nodense  25557  fobigcup  25654  axcontlem2  25808  onsucsuccmpi  26097  mblfinlem  26143  volsupnfl  26150  itg2addnc  26158  nn0prpwlem  26215  refref  26255  topmeet  26283  indexa  26325  sstotbnd2  26373  heiborlem7  26416  mzpclall  26674  dgraaf  27220  phisum  27386  stoweidlem57  27673  wallispilem3  27683  stirlinglem13  27702  bnj580  28990  bnj1384  29107  bnj1497  29135  isatliN  29785  atpsubN  30235  idldil  30596  cdleme50ldil  31030

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

This theorem depends on definitions:  df-bi 178  df-ral 2671