Theorem rgenw 2490

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

Syntax hints:   ∈ wcel 1481  ∀wral 2417

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

This theorem depends on definitions:  df-bi 116  df-ral 2422

This theorem is referenced by:  rgen2w  2491  reuun1  3363  0disj  3934  iinexgm  4087  epse  4272  xpiindim  4684  eliunxp  4686  opeliunxp2  4687  elrnmpti  4800  fnmpti  5259  mpoeq12  5839  iunex  6029  mpoex  6119  opeliunxp2f  6143  ixpssmap  6634  1domsn  6721  nneneq  6759  nqprrnd  7375  nqprdisj  7376  uzf  9353  sum0  11189  fisumcom2  11239  unennn  11946  tgidm  12282  tgrest  12377  txbas  12466  reldvg  12856  dvfvalap  12858  bj-indint  13300  bj-nn0suc0  13319  bj-nntrans  13320