Theorem rgenw 2605

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

This proof depends on syntax axioms:   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  rgen2w  2606  reuun1  3515  0disj  4127  iinexgm  4290  epse  4487  xpiindim  4917  eliunxp  4919  opeliunxp2  4920  elrnmpti  5035  fnmpti  5512  mpoeq12  6148  relmptopab  6291  iunex  6352  mpoex  6450  opeliunxp2f  6509  ixpssmap  7014  1domsn  7115  nneneq  7158  nqprrnd  7911  nqprdisj  7912  uzf  9934  hashfibclem  11298  sum0  12174  fisumcom2  12224  prod0  12371  fprodcom2fi  12412  phisum  13042  sumhashdc  13149  unennn  13340  prdsvallem  13674  prdsval  14257  fczpsrbag  15140  psr1clfi  15170  tgidm  15266  tgrest  15361  txbas  15450  reldvg  15871  dvfvalap  15873  bj-indint  17123  bj-nn0suc0  17142  bj-nntrans  17143