Theorem rgenw 2560

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

Syntax hints:   ∈ wcel 2175  ∀wral 2483

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 1471

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

This theorem is referenced by:  rgen2w  2561  reuun1  3454  0disj  4040  iinexgm  4197  epse  4388  xpiindim  4814  eliunxp  4816  opeliunxp2  4817  elrnmpti  4930  fnmpti  5403  mpoeq12  6004  iunex  6207  mpoex  6299  opeliunxp2f  6323  ixpssmap  6818  1domsn  6913  nneneq  6953  nqprrnd  7655  nqprdisj  7656  uzf  9650  sum0  11670  fisumcom2  11720  prod0  11867  fprodcom2fi  11908  phisum  12534  sumhashdc  12641  unennn  12739  prdsvallem  13075  prdsval  13076  fczpsrbag  14404  psr1clfi  14421  tgidm  14517  tgrest  14612  txbas  14701  reldvg  15122  dvfvalap  15124  bj-indint  15829  bj-nn0suc0  15848  bj-nntrans  15849