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  5789  opabex3  6273  oawordriexmid  6624  fifo  7158  inresflem  7238  0ct  7285  infnninf  7302  infnninfOLD  7303  exmidonfinlem  7382  pw1on  7422  netap  7451  2omotaplemap  7454  indpi  7540  nnindnn  8091  aptap  8808  sup3exmid  9115  nnssre  9125  nnind  9137  nnsub  9160  dfuzi  9568  indstr  9800  cnref1o  9858  frec2uzsucd  10635  uzsinds  10678  ser0f  10768  bccl  11001  wrdind  11270  rexuz3  11517  isumlessdc  12023  prodf1f  12070  iprodap0  12109  eff2  12207  reeff1  12227  prmind2  12658  3prm  12666  sqrt2irr  12700  phisum  12779  pockthi  12897  1arith  12906  1arith2  12907  prminf  13042  xpsff1o  13398  rngmgpf  13916  mgpf  13990  cnfld1  14552  cnsubglem  14559  isbasis3g  14736  distop  14775  cdivcncfap  15294  dveflem  15416  ioocosf1o  15544  2irrexpqap  15668  2sqlem6  15815  2sqlem10  15820  bj-indint  16377  bj-nnelirr  16399  bj-omord  16406  012of  16444  2o01f  16445  0nninf  16458  nconstwlpolem0  16519