Theorem rgen 2746

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

Syntax hints:   -> wi 4   e. wcel 1886   A.wral 2736

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

This theorem depends on definitions:  df-bi 189  df-ral 2741

This theorem is referenced by:  ralel  2747  rgenw  2748  mprg  2750  mprgbir  2751  r19.21be  2758  rgen2  2812  rgen2a  2814  rgen2aOLD  2815  nrex  2841  rexlimi  2868  rexlimiv  2872  sbcth2  3350  reuss  3723  r19.2zb  3858  ral0  3873  unimax  4232  mpteq1  4482  mpteq2ia  4484  reusv2lem4  4606  wfisg  5414  fnopab  5700  fmpti  6043  sorpssuni  6577  sorpssint  6578  onssmin  6621  tfis  6678  omssnlim  6703  finds  6716  finds2  6718  opabex3  6769  wfr3  7053  seqomlem2  7165  findcard3  7811  fifo  7943  fisupcl  7982  dfom3  8149  cantnfvalf  8167  rankf  8262  scottex  8353  cplem1  8357  harcard  8409  cardiun  8413  r0weon  8440  acnnum  8480  alephon  8497  alephsmo  8530  alephf1ALT  8531  alephfplem4  8535  dfac5lem4  8554  dfacacn  8568  kmlem1  8577  cflem  8673  cflecard  8680  cfsmolem  8697  fin23lem17  8765  hsmexlem4  8856  omina  9113  0tsk  9177  inar1  9197  wfgru  9238  reclem2pr  9470  nnssre  10610  dfnn2  10619  dfnn3  10620  nnind  10624  nnsub  10645  dfuzi  11023  uzinfmiOLD  11236  uzsupss  11253  cnref1o  11294  xrsupsslem  11589  xrinfmsslem  11590  xrsup0  11606  reltre  11627  rpltrp  11628  reltxrnmnf  11629  ser0f  12263  bccl  12504  hashkf  12514  hashbc  12613  wrdind  12828  sqrlem5  13303  rexuz3  13404  sqrtf  13419  ackbijnn  13879  incexclem  13887  prodf1f  13941  eff2  14146  reeff1  14167  sqrt2irr  14294  prmind2  14628  3prm  14634  pockthi  14844  infpn2  14850  prminf  14852  prmreclem2  14854  prmrec  14859  1arith  14864  1arith2  14865  vdwlem13  14936  ramz  14976  prmgap  15022  prmgaplcmOLD  15023  prmgaplcm  15024  prmgapprmo  15026  prmgapprmorOLD  15027  prmlem1a  15071  xpsff1o  15467  isacs1i  15556  dmaf  15937  cdaf  15938  coapm  15959  lublecllem  16227  pmtrdifel  17114  pmtrdifwrdel  17119  odf  17179  odfOLD  17195  efgrelexlemb  17393  dprd2da  17668  mgpf  17785  prdscrngd  17834  cnfld1  18986  cnsubglem  19010  cnmsubglem  19023  nn0srg  19030  rge0srg  19031  pmatcoe1fsupp  19718  isbasis3g  19957  basdif0  19961  distop  20004  mretopd  20101  2ndcsep  20467  refref  20521  kqf  20755  fbssfi  20845  filcon  20891  prdstmdd  21131  ustfilxp  21220  prdsxmslem2  21537  qdensere  21783  recld2  21825  ovolf  22428  dyadmax  22549  dveflem  22924  mdegxrf  23010  fta1  23254  vieta1  23258  aalioulem2  23282  taylfval  23307  pilem2  23400  pilem2OLD  23401  pilem3  23402  pilem3OLD  23403  recosf1o  23477  divlogrlim  23573  logcn  23585  ressatans  23853  leibpi  23861  ftalem3  23992  chtub  24133  2sqlem6  24290  2sqlem10  24295  chtppilim  24306  pntpbnd1  24417  pntlem3  24440  padicabvf  24462  axcontlem2  24988  isgrpoi  25919  cnid  26072  mulid  26077  cnrngo  26124  isvci  26194  isnvi  26225  ipasslem8  26471  hilid  26807  hlimf  26883  shsspwh  26892  pjrni  27348  pjmf1  27362  df0op2  27398  dfiop2  27399  hoaddcomi  27418  hoaddassi  27422  hocadddiri  27425  hocsubdiri  27426  hoaddid1i  27432  ho0coi  27434  hoid1i  27435  hoid1ri  27436  honegsubi  27442  hoddii  27635  lnopunilem2  27657  elunop2  27659  lnophm  27665  imaelshi  27704  cnlnadjlem8  27720  pjnmopi  27794  pjsdii  27801  pjddii  27802  pjtoi  27825  chirred  28041  nnindf  28375  nn0min  28377  esum2d  28907  dmvlsiga  28944  volmeas  29047  ddemeas  29052  sxbrsigalem3  29087  coinfliprv  29308  ballotlem7  29361  ballotlem7OLD  29399  signsw0glem  29435  bnj580  29717  bnj1384  29834  bnj1497  29862  kur14lem9  29930  msrf  30173  dfon2lem7  30428  frinsg  30476  bdayfo  30557  nodense  30571  fobigcup  30660  nn0prpwlem  30971  topmeet  31013  onsucsuccmpi  31096  taupilemrplb  31714  relowlssretop  31759  ptrecube  31933  poimirlem27  31960  heicant  31968  mblfinlem1  31970  volsupnfl  31978  dvtan  31985  itg2addnc  31989  indexa  32053  sstotbnd2  32099  heiborlem7  32142  atpsubN  33312  idldil  33673  cdleme50ldil  34109  mzpclall  35563  dgraaf  36005  dgraafOLD  36006  phisum  36070  arearect  36094  areaquad  36095  prmunb2  36653  radcnvrat  36657  upbdrech  37517  fsumiunss  37648  resincncf  37746  stoweidlem57  37912  wallispilem3  37923  stirlinglem13  37942  dirkertrigeqlem3  37956  fourierdlem62  38026  salexct  38187  salexct3  38195  salgencntex  38196  salgensscntex  38197  gsumge0cl  38207  0ome  38344  icoresmbl  38359  hoidmv1le  38410  tgoldbach  38905  2zlidl  39921  2zrngagrp  39930  2zrngnmlid  39936  crhmsubc  40067  drhmsubc  40069  drngcat  40070  fldcat  40071  fldhmsubc  40073  crhmsubcALTV  40086  drhmsubcALTV  40088  drngcatALTV  40089  fldcatALTV  40090  fldhmsubcALTV  40092  zlmodzxznm  40277  ldepsnlinc  40288  nn0sumshdiglem2  40420