Theorem rgenw 2376

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

Syntax hints:   ∈ wcel 1393  ∀wral 2306

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338

This theorem depends on definitions:  df-bi 110  df-ral 2311

This theorem is referenced by:  rgen2w  2377  reuun1  3219  0disj  3761  iinexgm  3908  epse  4079  xpiindim  4473  eliunxp  4475  opeliunxp2  4476  elrnmpti  4587  fnmpti  5027  mpt2eq12  5565  iunex  5750  mpt2ex  5836  nneneq  6320  nqprrnd  6641  nqprdisj  6642  uzf  8476  bj-indint  10055  bj-nn0suc0  10075  bj-nntrans  10076