Theorem rgen 2586

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 2516	. 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 2202   A.wral 2511

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 2516

This theorem is referenced by:  rgen2a  2587  rgenw  2588  mprg  2590  mprgbir  2591  rgen2  2619  r19.21be  2624  nrex  2625  rexlimi  2644  sbcth2  3121  reuss  3490  ral0  3598  unimax  3932  mpteq1  4178  mpteq2ia  4180  ordon  4590  tfis  4687  finds  4704  finds2  4705  ordom  4711  omsinds  4726  dmxpid  4959  fnopab  5464  fmpti  5807  opabex3  6293  oawordriexmid  6681  fifo  7222  inresflem  7302  0ct  7349  infnninf  7366  infnninfOLD  7367  exmidonfinlem  7447  pw1on  7487  netap  7516  2omotaplemap  7519  indpi  7605  nnindnn  8156  aptap  8872  sup3exmid  9179  nnssre  9189  nnind  9201  nnsub  9224  dfuzi  9634  indstr  9871  cnref1o  9929  frec2uzsucd  10709  uzsinds  10752  ser0f  10842  bccl  11075  wrdind  11352  rexuz3  11613  isumlessdc  12120  prodf1f  12167  iprodap0  12206  eff2  12304  reeff1  12324  prmind2  12755  3prm  12763  sqrt2irr  12797  phisum  12876  pockthi  12994  1arith  13003  1arith2  13004  prminf  13139  xpsff1o  13495  rngmgpf  14014  mgpf  14088  cnfld1  14651  cnsubglem  14658  isbasis3g  14840  distop  14879  cdivcncfap  15398  dveflem  15520  ioocosf1o  15648  2irrexpqap  15772  2sqlem6  15922  2sqlem10  15927  konigsberglem5  16416  bj-indint  16630  bj-nnelirr  16652  bj-omord  16659  012of  16696  2o01f  16697  0nninf  16713  nconstwlpolem0  16779