Theorem rgenw 2585

Description: Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
rgenw.1	|- ph

Assertion

Ref	Expression
rgenw	|- A. x e. A ph

Proof of Theorem rgenw

Step	Hyp	Ref	Expression
1		rgenw.1	. . 3 |- ph
2	1	a1i 9	. 2 |- ( x e. A -> ph )
3	2	rgen 2583	1 |- A. x e. A ph

Syntax hints:   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:  rgen2w  2586  reuun1  3486  0disj  4080  iinexgm  4238  epse  4433  xpiindim  4859  eliunxp  4861  opeliunxp2  4862  elrnmpti  4977  fnmpti  5452  mpoeq12  6070  relmptopab  6213  iunex  6274  mpoex  6366  opeliunxp2f  6390  ixpssmap  6887  1domsn  6984  nneneq  7026  nqprrnd  7741  nqprdisj  7742  uzf  9736  sum0  11915  fisumcom2  11965  prod0  12112  fprodcom2fi  12153  phisum  12779  sumhashdc  12886  unennn  12984  prdsvallem  13321  prdsval  13322  fczpsrbag  14651  psr1clfi  14668  tgidm  14764  tgrest  14859  txbas  14948  reldvg  15369  dvfvalap  15371  bj-indint  16377  bj-nn0suc0  16396  bj-nntrans  16397