Theorem rgenw 2552

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

Syntax hints:   e. wcel 2167   A.wral 2475

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 1463

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

This theorem is referenced by:  rgen2w  2553  reuun1  3445  0disj  4030  iinexgm  4187  epse  4377  xpiindim  4803  eliunxp  4805  opeliunxp2  4806  elrnmpti  4919  fnmpti  5386  mpoeq12  5982  iunex  6180  mpoex  6272  opeliunxp2f  6296  ixpssmap  6791  1domsn  6878  nneneq  6918  nqprrnd  7610  nqprdisj  7611  uzf  9604  sum0  11553  fisumcom2  11603  prod0  11750  fprodcom2fi  11791  phisum  12409  sumhashdc  12516  unennn  12614  fczpsrbag  14225  tgidm  14310  tgrest  14405  txbas  14494  reldvg  14915  dvfvalap  14917  bj-indint  15577  bj-nn0suc0  15596  bj-nntrans  15597