Theorem rgenw 2521

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

Syntax hints:   ∈ wcel 2136  ∀wral 2444

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 1437

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

This theorem is referenced by:  rgen2w  2522  reuun1  3404  0disj  3979  iinexgm  4133  epse  4320  xpiindim  4741  eliunxp  4743  opeliunxp2  4744  elrnmpti  4857  fnmpti  5316  mpoeq12  5902  iunex  6091  mpoex  6182  opeliunxp2f  6206  ixpssmap  6698  1domsn  6785  nneneq  6823  nqprrnd  7484  nqprdisj  7485  uzf  9469  sum0  11329  fisumcom2  11379  prod0  11526  fprodcom2fi  11567  phisum  12172  sumhashdc  12277  unennn  12330  tgidm  12714  tgrest  12809  txbas  12898  reldvg  13288  dvfvalap  13290  bj-indint  13813  bj-nn0suc0  13832  bj-nntrans  13833