Theorem rgen 2550

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

Syntax hints:   -> wi 4   e. wcel 2167   A.wral 2475

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 1463

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

This theorem is referenced by:  rgen2a  2551  rgenw  2552  mprg  2554  mprgbir  2555  rgen2  2583  r19.21be  2588  nrex  2589  rexlimi  2607  sbcth2  3077  reuss  3445  ral0  3553  unimax  3874  mpteq1  4118  mpteq2ia  4120  ordon  4523  tfis  4620  finds  4637  finds2  4638  ordom  4644  omsinds  4659  dmxpid  4888  fnopab  5383  fmpti  5715  opabex3  6180  oawordriexmid  6529  fifo  7047  inresflem  7127  0ct  7174  infnninf  7191  infnninfOLD  7192  exmidonfinlem  7262  pw1on  7295  netap  7323  2omotaplemap  7326  indpi  7411  nnindnn  7962  aptap  8679  sup3exmid  8986  nnssre  8996  nnind  9008  nnsub  9031  dfuzi  9438  indstr  9669  cnref1o  9727  frec2uzsucd  10495  uzsinds  10538  ser0f  10628  bccl  10861  rexuz3  11157  isumlessdc  11663  prodf1f  11710  iprodap0  11749  eff2  11847  reeff1  11867  prmind2  12298  3prm  12306  sqrt2irr  12340  phisum  12419  pockthi  12537  1arith  12546  1arith2  12547  prminf  12682  xpsff1o  13002  rngmgpf  13503  mgpf  13577  cnfld1  14138  cnsubglem  14145  isbasis3g  14292  distop  14331  cdivcncfap  14850  dveflem  14972  ioocosf1o  15100  2irrexpqap  15224  2sqlem6  15371  2sqlem10  15376  bj-indint  15587  bj-nnelirr  15609  bj-omord  15616  012of  15650  2o01f  15651  0nninf  15658  nconstwlpolem0  15717