Theorem rgenw 2461

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

Syntax hints:   e. wcel 1463   A.wral 2390

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1408

This theorem depends on definitions:  df-bi 116  df-ral 2395

This theorem is referenced by:  rgen2w  2462  reuun1  3324  0disj  3892  iinexgm  4039  epse  4224  xpiindim  4636  eliunxp  4638  opeliunxp2  4639  elrnmpti  4752  fnmpti  5209  mpoeq12  5785  iunex  5975  mpoex  6065  opeliunxp2f  6089  ixpssmap  6580  1domsn  6666  nneneq  6704  nqprrnd  7299  nqprdisj  7300  uzf  9231  sum0  11049  fisumcom2  11099  unennn  11755  tgidm  12086  tgrest  12181  txbas  12269  reldvg  12603  dvfvalap  12605  bj-indint  12821  bj-nn0suc0  12840  bj-nntrans  12841