Theorem rgen 2766

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

Syntax hints:   -> wi 4   e. wcel 1904   A.wral 2756

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

This theorem depends on definitions:  df-bi 190  df-ral 2761

This theorem is referenced by:  ralel  2767  rgenw  2768  mprg  2770  mprgbir  2771  r19.21be  2777  rgen2  2818  rgen2a  2820  nrex  2841  rexlimi  2864  rexlimiv  2867  sbcth2  3339  reuss  3715  r19.2zb  3850  ral0  3865  unimax  4225  mpteq1  4476  mpteq2ia  4478  reusv2lem4  4605  wfisg  5422  fnopab  5712  fmpti  6060  sorpssuni  6599  sorpssint  6600  onssmin  6643  tfis  6700  omssnlim  6725  finds  6738  finds2  6740  opabex3  6791  wfr3  7074  seqomlem2  7186  findcard3  7832  fifo  7964  fisupcl  8003  dfom3  8170  cantnfvalf  8188  rankf  8283  scottex  8374  cplem1  8378  harcard  8430  cardiun  8434  r0weon  8461  acnnum  8501  alephon  8518  alephsmo  8551  alephf1ALT  8552  alephfplem4  8556  dfac5lem4  8575  dfacacn  8589  kmlem1  8598  cflem  8694  cflecard  8701  cfsmolem  8718  fin23lem17  8786  hsmexlem4  8877  omina  9134  0tsk  9198  inar1  9218  wfgru  9259  reclem2pr  9491  nnssre  10635  dfnn2  10644  dfnn3  10645  nnind  10649  nnsub  10670  dfuzi  11049  uzinfmiOLD  11262  uzsupss  11279  cnref1o  11320  xrsupsslem  11617  xrinfmsslem  11618  xrsup0  11634  reltre  11655  rpltrp  11656  reltxrnmnf  11657  ser0f  12304  bccl  12545  hashkf  12555  hashbc  12657  wrdind  12887  sqrlem5  13387  rexuz3  13488  sqrtf  13503  ackbijnn  13963  incexclem  13971  prodf1f  14025  eff2  14230  reeff1  14251  sqrt2irr  14378  prmind2  14714  3prm  14720  pockthi  14930  infpn2  14936  prminf  14938  prmreclem2  14940  prmrec  14945  1arith  14950  1arith2  14951  vdwlem13  15022  ramz  15062  prmgap  15108  prmgaplcmOLD  15109  prmgaplcm  15110  prmgapprmo  15112  prmgapprmorOLD  15113  prmlem1a  15156  xpsff1o  15552  isacs1i  15641  dmaf  16022  cdaf  16023  coapm  16044  lublecllem  16312  pmtrdifel  17199  pmtrdifwrdel  17204  odf  17264  odfOLD  17280  efgrelexlemb  17478  dprd2da  17753  mgpf  17870  prdscrngd  17919  cnfld1  19070  cnsubglem  19094  cnmsubglem  19107  nn0srg  19114  rge0srg  19115  pmatcoe1fsupp  19802  isbasis3g  20041  basdif0  20045  distop  20088  mretopd  20185  2ndcsep  20551  refref  20605  kqf  20839  fbssfi  20930  filcon  20976  prdstmdd  21216  ustfilxp  21305  prdsxmslem2  21622  qdensere  21868  recld2  21910  ovolf  22513  dyadmax  22635  dveflem  23010  mdegxrf  23096  fta1  23340  vieta1  23344  aalioulem2  23368  taylfval  23393  pilem2  23486  pilem2OLD  23487  pilem3  23488  pilem3OLD  23489  recosf1o  23563  divlogrlim  23659  logcn  23671  ressatans  23939  leibpi  23947  ftalem3  24078  chtub  24219  2sqlem6  24376  2sqlem10  24381  chtppilim  24392  pntpbnd1  24503  pntlem3  24526  padicabvf  24548  axcontlem2  25074  isgrpoi  26007  cnid  26160  mulid  26165  cnrngo  26212  isvci  26282  isnvi  26313  ipasslem8  26559  hilid  26895  hlimf  26971  shsspwh  26980  pjrni  27436  pjmf1  27450  df0op2  27486  dfiop2  27487  hoaddcomi  27506  hoaddassi  27510  hocadddiri  27513  hocsubdiri  27514  hoaddid1i  27520  ho0coi  27522  hoid1i  27523  hoid1ri  27524  honegsubi  27530  hoddii  27723  lnopunilem2  27745  elunop2  27747  lnophm  27753  imaelshi  27792  cnlnadjlem8  27808  pjnmopi  27882  pjsdii  27889  pjddii  27890  pjtoi  27913  chirred  28129  nnindf  28457  nn0min  28459  esum2d  28988  dmvlsiga  29025  volmeas  29127  ddemeas  29132  sxbrsigalem3  29167  coinfliprv  29388  ballotlem7  29441  ballotlem7OLD  29479  signsw0glem  29514  bnj580  29796  bnj1384  29913  bnj1497  29941  kur14lem9  30009  msrf  30252  dfon2lem7  30506  frinsg  30554  bdayfo  30635  nodense  30649  fobigcup  30738  nn0prpwlem  31049  topmeet  31091  onsucsuccmpi  31174  taupilemrplb  31791  relowlssretop  31836  ptrecube  32004  poimirlem27  32031  heicant  32039  mblfinlem1  32041  volsupnfl  32049  dvtan  32056  itg2addnc  32060  indexa  32124  sstotbnd2  32170  heiborlem7  32213  atpsubN  33389  idldil  33750  cdleme50ldil  34186  mzpclall  35640  dgraaf  36082  dgraafOLD  36083  phisum  36147  arearect  36171  areaquad  36172  prmunb2  36729  radcnvrat  36733  unirnmapsn  37567  ssmapsn  37569  upbdrech  37611  fsumiunss  37750  resincncf  37849  dmvolss  37960  volioof  37962  stoweidlem57  38030  wallispilem3  38041  stirlinglem13  38060  dirkertrigeqlem3  38074  fourierdlem62  38144  salexct  38305  salexct3  38313  salgencntex  38314  salgensscntex  38315  gsumge0cl  38327  0ome  38469  icoresmbl  38483  hoidmv1le  38534  tgoldbach  39056  nbgrnself  39593  2zlidl  40442  2zrngagrp  40451  2zrngnmlid  40457  crhmsubc  40588  drhmsubc  40590  drngcat  40591  fldcat  40592  fldhmsubc  40594  crhmsubcALTV  40607  drhmsubcALTV  40609  drngcatALTV  40610  fldcatALTV  40611  fldhmsubcALTV  40613  zlmodzxznm  40798  ldepsnlinc  40809  nn0sumshdiglem2  40941