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  3117  reuss  3485  ral0  3593  unimax  3922  mpteq1  4168  mpteq2ia  4170  ordon  4578  tfis  4675  finds  4692  finds2  4693  ordom  4699  omsinds  4714  dmxpid  4945  fnopab  5448  fmpti  5787  opabex3  6267  oawordriexmid  6616  fifo  7147  inresflem  7227  0ct  7274  infnninf  7291  infnninfOLD  7292  exmidonfinlem  7371  pw1on  7411  netap  7440  2omotaplemap  7443  indpi  7529  nnindnn  8080  aptap  8797  sup3exmid  9104  nnssre  9114  nnind  9126  nnsub  9149  dfuzi  9557  indstr  9788  cnref1o  9846  frec2uzsucd  10623  uzsinds  10666  ser0f  10756  bccl  10989  wrdind  11254  rexuz3  11501  isumlessdc  12007  prodf1f  12054  iprodap0  12093  eff2  12191  reeff1  12211  prmind2  12642  3prm  12650  sqrt2irr  12684  phisum  12763  pockthi  12881  1arith  12890  1arith2  12891  prminf  13026  xpsff1o  13382  rngmgpf  13900  mgpf  13974  cnfld1  14536  cnsubglem  14543  isbasis3g  14720  distop  14759  cdivcncfap  15278  dveflem  15400  ioocosf1o  15528  2irrexpqap  15652  2sqlem6  15799  2sqlem10  15804  bj-indint  16294  bj-nnelirr  16316  bj-omord  16323  012of  16357  2o01f  16358  0nninf  16370  nconstwlpolem0  16431