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  5385  fmpti  5717  opabex3  6188  oawordriexmid  6537  fifo  7055  inresflem  7135  0ct  7182  infnninf  7199  infnninfOLD  7200  exmidonfinlem  7272  pw1on  7309  netap  7337  2omotaplemap  7340  indpi  7426  nnindnn  7977  aptap  8694  sup3exmid  9001  nnssre  9011  nnind  9023  nnsub  9046  dfuzi  9453  indstr  9684  cnref1o  9742  frec2uzsucd  10510  uzsinds  10553  ser0f  10643  bccl  10876  rexuz3  11172  isumlessdc  11678  prodf1f  11725  iprodap0  11764  eff2  11862  reeff1  11882  prmind2  12313  3prm  12321  sqrt2irr  12355  phisum  12434  pockthi  12552  1arith  12561  1arith2  12562  prminf  12697  xpsff1o  13051  rngmgpf  13569  mgpf  13643  cnfld1  14204  cnsubglem  14211  isbasis3g  14366  distop  14405  cdivcncfap  14924  dveflem  15046  ioocosf1o  15174  2irrexpqap  15298  2sqlem6  15445  2sqlem10  15450  bj-indint  15661  bj-nnelirr  15683  bj-omord  15690  012of  15724  2o01f  15725  0nninf  15735  nconstwlpolem0  15794