Theorem rgen 2603

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  rgen2a  2604  rgenw  2605  mprg  2607  mprgbir  2608  rgen2  2636  r19.21be  2641  nrex  2642  rexlimi  2661  sbcth2  3140  reuss  3514  ral0  3629  unimax  3969  mpteq1  4216  mpteq2ia  4219  ordon  4635  tfis  4732  finds  4749  finds2  4750  ordom  4756  omsinds  4771  dmxpid  5005  fnopab  5511  fmpti  5863  opabex3  6355  oawordriexmid  6747  fifo  7319  inresflem  7406  0ct  7453  infnninf  7470  infnninfOLD  7471  exmidonfinlem  7551  pw1on  7591  netap  7626  2omotaplemap  7629  indpi  7715  nnindnn  8266  aptap  8986  sup3exmid  9295  nnssre  9317  nnind  9329  nnsub  9352  dfuzi  9767  indstr  10009  cnref1o  10068  frec2uzsucd  10859  uzsinds  10902  ser0f  10992  bccl  11227  hashfibc  11305  wrdind  11516  rexuz3  11778  isumlessdc  12288  prodf1f  12335  iprodap0  12374  eff2  12472  reeff1  12492  prmind2  12923  3prm  12931  sqrt2irr  12966  phisum  13048  pockthi  13166  1arith  13175  1arith2  13176  prmlem1a  13250  ballotfilemofi  13277  ballotfilem2  13286  ballotfilemefi  13295  ballotfilemafi  13296  ballotfilembfi  13297  ballotfilem7  13337  prminf  13404  xpsff1o  13729  rngmgpf  14343  mgpf  14422  cnfld1  15018  cnsubglem  15025  isbasis3g  15272  distop  15311  cdivcncfap  15830  dveflem  15952  ioocosf1o  16082  2irrexpqap  16214  chtqub  16296  2sqlem6  16444  2sqlem10  16449  konigsberglem5  16938  bj-indint  17162  bj-nnelirr  17184  bj-omord  17191  012of  17228  2o01f  17229  0nninf  17253  nconstwlpolem0  17320