Theorem rgenw 2532

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

Syntax hints:   ∈ wcel 2148  ∀wral 2455

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 1449

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

This theorem is referenced by:  rgen2w  2533  reuun1  3418  0disj  4001  iinexgm  4155  epse  4343  xpiindim  4765  eliunxp  4767  opeliunxp2  4768  elrnmpti  4881  fnmpti  5345  mpoeq12  5935  iunex  6124  mpoex  6215  opeliunxp2f  6239  ixpssmap  6732  1domsn  6819  nneneq  6857  nqprrnd  7542  nqprdisj  7543  uzf  9531  sum0  11396  fisumcom2  11446  prod0  11593  fprodcom2fi  11634  phisum  12240  sumhashdc  12345  unennn  12398  tgidm  13577  tgrest  13672  txbas  13761  reldvg  14151  dvfvalap  14153  bj-indint  14686  bj-nn0suc0  14705  bj-nntrans  14706