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  6064  relmptopab  6207  iunex  6268  mpoex  6360  opeliunxp2f  6384  ixpssmap  6879  1domsn  6976  nneneq  7018  nqprrnd  7730  nqprdisj  7731  uzf  9725  sum0  11899  fisumcom2  11949  prod0  12096  fprodcom2fi  12137  phisum  12763  sumhashdc  12870  unennn  12968  prdsvallem  13305  prdsval  13306  fczpsrbag  14635  psr1clfi  14652  tgidm  14748  tgrest  14843  txbas  14932  reldvg  15353  dvfvalap  15355  bj-indint  16294  bj-nn0suc0  16313  bj-nntrans  16314