Theorem rgenw 2549

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

Syntax hints:   e. wcel 2164   A.wral 2472

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 1460

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

This theorem is referenced by:  rgen2w  2550  reuun1  3441  0disj  4026  iinexgm  4183  epse  4373  xpiindim  4799  eliunxp  4801  opeliunxp2  4802  elrnmpti  4915  fnmpti  5382  mpoeq12  5978  iunex  6175  mpoex  6267  opeliunxp2f  6291  ixpssmap  6786  1domsn  6873  nneneq  6913  nqprrnd  7603  nqprdisj  7604  uzf  9595  sum0  11531  fisumcom2  11581  prod0  11728  fprodcom2fi  11769  phisum  12378  sumhashdc  12485  unennn  12554  fczpsrbag  14157  tgidm  14242  tgrest  14337  txbas  14426  reldvg  14833  dvfvalap  14835  bj-indint  15423  bj-nn0suc0  15442  bj-nntrans  15443