Theorem rgen 2583

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

Syntax hints:   -> wi 4   e. wcel 2200   A.wral 2508

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 1495

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

This theorem is referenced by:  rgen2a  2584  rgenw  2585  mprg  2587  mprgbir  2588  rgen2  2616  r19.21be  2621  nrex  2622  rexlimi  2641  sbcth2  3118  reuss  3486  ral0  3594  unimax  3925  mpteq1  4171  mpteq2ia  4173  ordon  4582  tfis  4679  finds  4696  finds2  4697  ordom  4703  omsinds  4718  dmxpid  4951  fnopab  5454  fmpti  5795  opabex3  6279  oawordriexmid  6633  fifo  7170  inresflem  7250  0ct  7297  infnninf  7314  infnninfOLD  7315  exmidonfinlem  7394  pw1on  7434  netap  7463  2omotaplemap  7466  indpi  7552  nnindnn  8103  aptap  8820  sup3exmid  9127  nnssre  9137  nnind  9149  nnsub  9172  dfuzi  9580  indstr  9817  cnref1o  9875  frec2uzsucd  10653  uzsinds  10696  ser0f  10786  bccl  11019  wrdind  11293  rexuz3  11541  isumlessdc  12047  prodf1f  12094  iprodap0  12133  eff2  12231  reeff1  12251  prmind2  12682  3prm  12690  sqrt2irr  12724  phisum  12803  pockthi  12921  1arith  12930  1arith2  12931  prminf  13066  xpsff1o  13422  rngmgpf  13940  mgpf  14014  cnfld1  14576  cnsubglem  14583  isbasis3g  14760  distop  14799  cdivcncfap  15318  dveflem  15440  ioocosf1o  15568  2irrexpqap  15692  2sqlem6  15839  2sqlem10  15844  bj-indint  16462  bj-nnelirr  16484  bj-omord  16491  012of  16528  2o01f  16529  0nninf  16542  nconstwlpolem0  16603