Theorem rgen 2595

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

Syntax hints:   -> wi 4   e. wcel 2203   A.wral 2520

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 1498

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

This theorem is referenced by:  rgen2a  2596  rgenw  2597  mprg  2599  mprgbir  2600  rgen2  2628  r19.21be  2633  nrex  2634  rexlimi  2653  sbcth2  3131  reuss  3502  ral0  3611  unimax  3948  mpteq1  4194  mpteq2ia  4196  ordon  4608  tfis  4705  finds  4722  finds2  4723  ordom  4729  omsinds  4744  dmxpid  4978  fnopab  5483  fmpti  5829  opabex3  6315  oawordriexmid  6703  fifo  7267  inresflem  7351  0ct  7398  infnninf  7415  infnninfOLD  7416  exmidonfinlem  7496  pw1on  7536  netap  7568  2omotaplemap  7571  indpi  7657  nnindnn  8208  aptap  8924  sup3exmid  9231  nnssre  9241  nnind  9253  nnsub  9276  dfuzi  9688  indstr  9925  cnref1o  9983  frec2uzsucd  10763  uzsinds  10806  ser0f  10896  bccl  11129  hashfibc  11207  wrdind  11414  rexuz3  11675  isumlessdc  12182  prodf1f  12229  iprodap0  12268  eff2  12366  reeff1  12386  prmind2  12817  3prm  12825  sqrt2irr  12859  phisum  12938  pockthi  13056  1arith  13065  1arith2  13066  ballotfilemofi  13138  ballotfilem2  13142  prminf  13206  xpsff1o  13562  rngmgpf  14081  mgpf  14155  cnfld1  14720  cnsubglem  14727  isbasis3g  14911  distop  14950  cdivcncfap  15469  dveflem  15591  ioocosf1o  15719  2irrexpqap  15843  2sqlem6  15993  2sqlem10  15998  konigsberglem5  16487  bj-indint  16701  bj-nnelirr  16723  bj-omord  16730  012of  16767  2o01f  16768  0nninf  16782  nconstwlpolem0  16849