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  6283  oawordriexmid  6637  fifo  7178  inresflem  7258  0ct  7305  infnninf  7322  infnninfOLD  7323  exmidonfinlem  7403  pw1on  7443  netap  7472  2omotaplemap  7475  indpi  7561  nnindnn  8112  aptap  8829  sup3exmid  9136  nnssre  9146  nnind  9158  nnsub  9181  dfuzi  9589  indstr  9826  cnref1o  9884  frec2uzsucd  10662  uzsinds  10705  ser0f  10795  bccl  11028  wrdind  11302  rexuz3  11550  isumlessdc  12056  prodf1f  12103  iprodap0  12142  eff2  12240  reeff1  12260  prmind2  12691  3prm  12699  sqrt2irr  12733  phisum  12812  pockthi  12930  1arith  12939  1arith2  12940  prminf  13075  xpsff1o  13431  rngmgpf  13949  mgpf  14023  cnfld1  14585  cnsubglem  14592  isbasis3g  14769  distop  14808  cdivcncfap  15327  dveflem  15449  ioocosf1o  15577  2irrexpqap  15701  2sqlem6  15848  2sqlem10  15853  bj-indint  16526  bj-nnelirr  16548  bj-omord  16555  012of  16592  2o01f  16593  0nninf  16606  nconstwlpolem0  16667