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  3444  ral0  3552  unimax  3873  mpteq1  4117  mpteq2ia  4119  ordon  4522  tfis  4619  finds  4636  finds2  4637  ordom  4643  omsinds  4658  dmxpid  4887  fnopab  5382  fmpti  5714  opabex3  6179  oawordriexmid  6528  fifo  7046  inresflem  7126  0ct  7173  infnninf  7190  infnninfOLD  7191  exmidonfinlem  7260  pw1on  7293  netap  7321  2omotaplemap  7324  indpi  7409  nnindnn  7960  aptap  8677  sup3exmid  8984  nnssre  8994  nnind  9006  nnsub  9029  dfuzi  9436  indstr  9667  cnref1o  9725  frec2uzsucd  10493  uzsinds  10536  ser0f  10626  bccl  10859  rexuz3  11155  isumlessdc  11661  prodf1f  11708  iprodap0  11747  eff2  11845  reeff1  11865  prmind2  12288  3prm  12296  sqrt2irr  12330  phisum  12409  pockthi  12527  1arith  12536  1arith2  12537  prminf  12672  xpsff1o  12992  rngmgpf  13493  mgpf  13567  cnfld1  14128  cnsubglem  14135  isbasis3g  14282  distop  14321  cdivcncfap  14840  dveflem  14962  ioocosf1o  15090  2irrexpqap  15214  2sqlem6  15361  2sqlem10  15366  bj-indint  15577  bj-nnelirr  15599  bj-omord  15606  012of  15640  2o01f  15641  0nninf  15648  nconstwlpolem0  15707