Theorem rgen 2485

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

Syntax hints:   -> wi 4   e. wcel 1480   A.wral 2416

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

This theorem depends on definitions:  df-bi 116  df-ral 2421

This theorem is referenced by:  rgen2a  2486  rgenw  2487  mprg  2489  mprgbir  2490  rgen2  2518  r19.21be  2523  nrex  2524  rexlimi  2542  sbcth2  2996  reuss  3357  ral0  3464  unimax  3770  mpteq1  4012  mpteq2ia  4014  ordon  4402  tfis  4497  finds  4514  finds2  4515  ordom  4520  omsinds  4535  dmxpid  4760  fnopab  5247  fmpti  5572  opabex3  6020  oawordriexmid  6366  fifo  6868  inresflem  6945  0ct  6992  infnninf  7022  exmidonfinlem  7049  indpi  7150  nnindnn  7701  sup3exmid  8715  nnssre  8724  nnind  8736  nnsub  8759  dfuzi  9161  indstr  9388  cnref1o  9440  frec2uzsucd  10174  uzsinds  10215  ser0f  10288  bccl  10513  rexuz3  10762  isumlessdc  11265  prodf1f  11312  eff2  11386  reeff1  11407  prmind2  11801  3prm  11809  sqrt2irr  11840  isbasis3g  12213  distop  12254  cdivcncfap  12756  dveflem  12855  bj-indint  13129  bj-nnelirr  13151  bj-omord  13158  0nninf  13197  isomninnlem  13225