Theorem rgenw 2585

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

Syntax hints:   ∈ wcel 2200  ∀wral 2508

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 1495

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

This theorem is referenced by:  rgen2w  2586  reuun1  3487  0disj  4083  iinexgm  4242  epse  4437  xpiindim  4865  eliunxp  4867  opeliunxp2  4868  elrnmpti  4983  fnmpti  5458  mpoeq12  6076  relmptopab  6219  iunex  6280  mpoex  6374  opeliunxp2f  6399  ixpssmap  6896  1domsn  6996  nneneq  7038  nqprrnd  7753  nqprdisj  7754  uzf  9748  sum0  11939  fisumcom2  11989  prod0  12136  fprodcom2fi  12177  phisum  12803  sumhashdc  12910  unennn  13008  prdsvallem  13345  prdsval  13346  fczpsrbag  14675  psr1clfi  14692  tgidm  14788  tgrest  14883  txbas  14972  reldvg  15393  dvfvalap  15395  bj-indint  16462  bj-nn0suc0  16481  bj-nntrans  16482