Theorem rgenw 2430

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 2428	1 ⊢ ∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   ∈ wcel 1438  ∀wral 2359

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

This theorem depends on definitions:  df-bi 115  df-ral 2364

This theorem is referenced by:  rgen2w  2431  reuun1  3281  0disj  3840  iinexgm  3988  epse  4167  xpiindim  4569  eliunxp  4571  opeliunxp2  4572  elrnmpti  4684  fnmpti  5136  mpt2eq12  5701  iunex  5886  mpt2ex  5972  opeliunxp2f  5995  1domsn  6525  nneneq  6563  nqprrnd  7092  nqprdisj  7093  uzf  9012  sum0  10767  fisumcom2  10819  unennn  11475  bj-indint  11709  bj-nn0suc0  11728  bj-nntrans  11729