Theorem rgen 2597

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

Syntax hints:   -> wi 4   e. wcel 2205   A.wral 2522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1498

This theorem depends on definitions:  df-bi 117  df-ral 2527

This theorem is referenced by:  rgen2a  2598  rgenw  2599  mprg  2601  mprgbir  2602  rgen2  2630  r19.21be  2635  nrex  2636  rexlimi  2655  sbcth2  3134  reuss  3506  ral0  3615  unimax  3953  mpteq1  4199  mpteq2ia  4201  ordon  4613  tfis  4710  finds  4727  finds2  4728  ordom  4734  omsinds  4749  dmxpid  4983  fnopab  5488  fmpti  5834  opabex3  6324  oawordriexmid  6716  fifo  7280  inresflem  7364  0ct  7411  infnninf  7428  infnninfOLD  7429  exmidonfinlem  7509  pw1on  7549  netap  7584  2omotaplemap  7587  indpi  7673  nnindnn  8224  aptap  8941  sup3exmid  9248  nnssre  9258  nnind  9270  nnsub  9293  dfuzi  9706  indstr  9943  cnref1o  10001  frec2uzsucd  10787  uzsinds  10830  ser0f  10920  bccl  11154  hashfibc  11232  wrdind  11439  rexuz3  11700  isumlessdc  12207  prodf1f  12254  iprodap0  12293  eff2  12391  reeff1  12411  prmind2  12842  3prm  12850  sqrt2irr  12884  phisum  12963  pockthi  13081  1arith  13090  1arith2  13091  ballotfilemofi  13163  ballotfilem2  13172  ballotfilemefi  13181  ballotfilemafi  13182  ballotfilembfi  13183  ballotfilem7  13223  prminf  13290  xpsff1o  13613  rngmgpf  14176  mgpf  14254  cnfld1  14846  cnsubglem  14853  isbasis3g  15037  distop  15076  cdivcncfap  15595  dveflem  15717  ioocosf1o  15845  2irrexpqap  15969  2sqlem6  16119  2sqlem10  16124  konigsberglem5  16613  bj-indint  16827  bj-nnelirr  16849  bj-omord  16856  012of  16893  2o01f  16894  0nninf  16908  nconstwlpolem0  16975