Theorem rgen 2559

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

Syntax hints:   -> wi 4   e. wcel 2176   A.wral 2484

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 1472

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

This theorem is referenced by:  rgen2a  2560  rgenw  2561  mprg  2563  mprgbir  2564  rgen2  2592  r19.21be  2597  nrex  2598  rexlimi  2616  sbcth2  3086  reuss  3454  ral0  3562  unimax  3884  mpteq1  4129  mpteq2ia  4131  ordon  4535  tfis  4632  finds  4649  finds2  4650  ordom  4656  omsinds  4671  dmxpid  4900  fnopab  5402  fmpti  5734  opabex3  6209  oawordriexmid  6558  fifo  7084  inresflem  7164  0ct  7211  infnninf  7228  infnninfOLD  7229  exmidonfinlem  7303  pw1on  7340  netap  7368  2omotaplemap  7371  indpi  7457  nnindnn  8008  aptap  8725  sup3exmid  9032  nnssre  9042  nnind  9054  nnsub  9077  dfuzi  9485  indstr  9716  cnref1o  9774  frec2uzsucd  10548  uzsinds  10591  ser0f  10681  bccl  10914  rexuz3  11334  isumlessdc  11840  prodf1f  11887  iprodap0  11926  eff2  12024  reeff1  12044  prmind2  12475  3prm  12483  sqrt2irr  12517  phisum  12596  pockthi  12714  1arith  12723  1arith2  12724  prminf  12859  xpsff1o  13214  rngmgpf  13732  mgpf  13806  cnfld1  14367  cnsubglem  14374  isbasis3g  14551  distop  14590  cdivcncfap  15109  dveflem  15231  ioocosf1o  15359  2irrexpqap  15483  2sqlem6  15630  2sqlem10  15635  bj-indint  15904  bj-nnelirr  15926  bj-omord  15933  012of  15967  2o01f  15968  0nninf  15978  nconstwlpolem0  16039