Theorem rgen 2561

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

Syntax hints:   -> wi 4   e. wcel 2178   A.wral 2486

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 1473

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

This theorem is referenced by:  rgen2a  2562  rgenw  2563  mprg  2565  mprgbir  2566  rgen2  2594  r19.21be  2599  nrex  2600  rexlimi  2618  sbcth2  3094  reuss  3462  ral0  3570  unimax  3898  mpteq1  4144  mpteq2ia  4146  ordon  4552  tfis  4649  finds  4666  finds2  4667  ordom  4673  omsinds  4688  dmxpid  4918  fnopab  5420  fmpti  5755  opabex3  6230  oawordriexmid  6579  fifo  7108  inresflem  7188  0ct  7235  infnninf  7252  infnninfOLD  7253  exmidonfinlem  7332  pw1on  7372  netap  7401  2omotaplemap  7404  indpi  7490  nnindnn  8041  aptap  8758  sup3exmid  9065  nnssre  9075  nnind  9087  nnsub  9110  dfuzi  9518  indstr  9749  cnref1o  9807  frec2uzsucd  10583  uzsinds  10626  ser0f  10716  bccl  10949  wrdind  11213  rexuz3  11416  isumlessdc  11922  prodf1f  11969  iprodap0  12008  eff2  12106  reeff1  12126  prmind2  12557  3prm  12565  sqrt2irr  12599  phisum  12678  pockthi  12796  1arith  12805  1arith2  12806  prminf  12941  xpsff1o  13296  rngmgpf  13814  mgpf  13888  cnfld1  14449  cnsubglem  14456  isbasis3g  14633  distop  14672  cdivcncfap  15191  dveflem  15313  ioocosf1o  15441  2irrexpqap  15565  2sqlem6  15712  2sqlem10  15717  bj-indint  16066  bj-nnelirr  16088  bj-omord  16095  012of  16130  2o01f  16131  0nninf  16143  nconstwlpolem0  16204