Theorem rgenw 2532

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 2530	1 |- A. x e. A ph

Syntax hints:   e. wcel 2148   A.wral 2455

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 1449

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

This theorem is referenced by:  rgen2w  2533  reuun1  3419  0disj  4002  iinexgm  4156  epse  4344  xpiindim  4766  eliunxp  4768  opeliunxp2  4769  elrnmpti  4882  fnmpti  5346  mpoeq12  5937  iunex  6126  mpoex  6217  opeliunxp2f  6241  ixpssmap  6734  1domsn  6821  nneneq  6859  nqprrnd  7544  nqprdisj  7545  uzf  9533  sum0  11398  fisumcom2  11448  prod0  11595  fprodcom2fi  11636  phisum  12242  sumhashdc  12347  unennn  12400  tgidm  13659  tgrest  13754  txbas  13843  reldvg  14233  dvfvalap  14235  bj-indint  14768  bj-nn0suc0  14787  bj-nntrans  14788