Theorem rgenw 2418

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

Syntax hints:   ∈ wcel 1433  ∀wral 2348

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 1378

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

This theorem is referenced by:  rgen2w  2419  reuun1  3246  0disj  3782  iinexgm  3929  epse  4097  xpiindim  4491  eliunxp  4493  opeliunxp2  4494  elrnmpti  4605  fnmpti  5047  mpt2eq12  5585  iunex  5770  mpt2ex  5856  nneneq  6343  nqprrnd  6733  nqprdisj  6734  uzf  8622  bj-indint  10726  bj-nn0suc0  10745  bj-nntrans  10746