Theorem rgenw 2561

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

Syntax hints:   e. wcel 2176   A.wral 2484

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 1472

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

This theorem is referenced by:  rgen2w  2562  reuun1  3455  0disj  4042  iinexgm  4199  epse  4390  xpiindim  4816  eliunxp  4818  opeliunxp2  4819  elrnmpti  4932  fnmpti  5406  mpoeq12  6007  iunex  6210  mpoex  6302  opeliunxp2f  6326  ixpssmap  6821  1domsn  6916  nneneq  6956  nqprrnd  7658  nqprdisj  7659  uzf  9653  sum0  11732  fisumcom2  11782  prod0  11929  fprodcom2fi  11970  phisum  12596  sumhashdc  12703  unennn  12801  prdsvallem  13137  prdsval  13138  fczpsrbag  14466  psr1clfi  14483  tgidm  14579  tgrest  14674  txbas  14763  reldvg  15184  dvfvalap  15186  bj-indint  15904  bj-nn0suc0  15923  bj-nntrans  15924