Theorem rgen 2585

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

Syntax hints:   -> wi 4   e. wcel 2202   A.wral 2510

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 1497

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

This theorem is referenced by:  rgen2a  2586  rgenw  2587  mprg  2589  mprgbir  2590  rgen2  2618  r19.21be  2623  nrex  2624  rexlimi  2643  sbcth2  3120  reuss  3488  ral0  3596  unimax  3927  mpteq1  4173  mpteq2ia  4175  ordon  4584  tfis  4681  finds  4698  finds2  4699  ordom  4705  omsinds  4720  dmxpid  4953  fnopab  5457  fmpti  5799  opabex3  6284  oawordriexmid  6638  fifo  7179  inresflem  7259  0ct  7306  infnninf  7323  infnninfOLD  7324  exmidonfinlem  7404  pw1on  7444  netap  7473  2omotaplemap  7476  indpi  7562  nnindnn  8113  aptap  8830  sup3exmid  9137  nnssre  9147  nnind  9159  nnsub  9182  dfuzi  9590  indstr  9827  cnref1o  9885  frec2uzsucd  10664  uzsinds  10707  ser0f  10797  bccl  11030  wrdind  11307  rexuz3  11568  isumlessdc  12075  prodf1f  12122  iprodap0  12161  eff2  12259  reeff1  12279  prmind2  12710  3prm  12718  sqrt2irr  12752  phisum  12831  pockthi  12949  1arith  12958  1arith2  12959  prminf  13094  xpsff1o  13450  rngmgpf  13969  mgpf  14043  cnfld1  14605  cnsubglem  14612  isbasis3g  14789  distop  14828  cdivcncfap  15347  dveflem  15469  ioocosf1o  15597  2irrexpqap  15721  2sqlem6  15868  2sqlem10  15873  konigsberglem5  16362  bj-indint  16577  bj-nnelirr  16599  bj-omord  16606  012of  16643  2o01f  16644  0nninf  16657  nconstwlpolem0  16719