Theorem rgenw 2605

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

Syntax hints:   ∈ wcel 2209  ∀wral 2528

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 1502

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

This theorem is referenced by:  rgen2w  2606  reuun1  3515  0disj  4122  iinexgm  4285  epse  4482  xpiindim  4912  eliunxp  4914  opeliunxp2  4915  elrnmpti  5030  fnmpti  5507  mpoeq12  6138  relmptopab  6281  iunex  6342  mpoex  6440  opeliunxp2f  6499  ixpssmap  7004  1domsn  7105  nneneq  7148  nqprrnd  7900  nqprdisj  7901  uzf  9903  hashfibclem  11260  sum0  12133  fisumcom2  12183  prod0  12330  fprodcom2fi  12371  phisum  12997  sumhashdc  13104  unennn  13266  prdsvallem  13598  prdsval  14150  fczpsrbag  14979  psr1clfi  15002  tgidm  15098  tgrest  15193  txbas  15282  reldvg  15703  dvfvalap  15705  bj-indint  16871  bj-nn0suc0  16890  bj-nntrans  16891