Theorem rgenw 2485

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

Syntax hints:   e. wcel 1480   A.wral 2414

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

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

This theorem is referenced by:  rgen2w  2486  reuun1  3353  0disj  3921  iinexgm  4074  epse  4259  xpiindim  4671  eliunxp  4673  opeliunxp2  4674  elrnmpti  4787  fnmpti  5246  mpoeq12  5824  iunex  6014  mpoex  6104  opeliunxp2f  6128  ixpssmap  6619  1domsn  6706  nneneq  6744  nqprrnd  7344  nqprdisj  7345  uzf  9322  sum0  11150  fisumcom2  11200  unennn  11899  tgidm  12232  tgrest  12327  txbas  12416  reldvg  12806  dvfvalap  12808  bj-indint  13118  bj-nn0suc0  13137  bj-nntrans  13138