Theorem rgenw 2599

Description: Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
rgenw.1	⊢ 𝜑

Assertion

Ref	Expression
rgenw	⊢ ∀𝑥 ∈ 𝐴 𝜑

Proof of Theorem rgenw

Step	Hyp	Ref	Expression
1		rgenw.1	. . 3 ⊢ 𝜑
2	1	a1i 9	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝜑)
3	2	rgen 2597	1 ⊢ ∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   ∈ wcel 2205  ∀wral 2522

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 1498

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

This theorem is referenced by:  rgen2w  2600  reuun1  3507  0disj  4111  iinexgm  4271  epse  4468  xpiindim  4897  eliunxp  4899  opeliunxp2  4900  elrnmpti  5015  fnmpti  5492  mpoeq12  6121  relmptopab  6264  iunex  6325  mpoex  6423  opeliunxp2f  6482  ixpssmap  6980  1domsn  7081  nneneq  7124  nqprrnd  7874  nqprdisj  7875  uzf  9874  hashfibclem  11231  sum0  12099  fisumcom2  12149  prod0  12296  fprodcom2fi  12337  phisum  12963  sumhashdc  13070  unennn  13232  prdsvallem  13564  prdsval  14115  fczpsrbag  14946  psr1clfi  14969  tgidm  15065  tgrest  15160  txbas  15249  reldvg  15670  dvfvalap  15672  bj-indint  16827  bj-nn0suc0  16846  bj-nntrans  16847