Theorem rgenw 2561

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

Syntax hints:   ∈ wcel 2176  ∀wral 2484

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 1472

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

This theorem is referenced by:  rgen2w  2562  reuun1  3455  0disj  4041  iinexgm  4198  epse  4389  xpiindim  4815  eliunxp  4817  opeliunxp2  4818  elrnmpti  4931  fnmpti  5404  mpoeq12  6005  iunex  6208  mpoex  6300  opeliunxp2f  6324  ixpssmap  6819  1domsn  6914  nneneq  6954  nqprrnd  7656  nqprdisj  7657  uzf  9651  sum0  11699  fisumcom2  11749  prod0  11896  fprodcom2fi  11937  phisum  12563  sumhashdc  12670  unennn  12768  prdsvallem  13104  prdsval  13105  fczpsrbag  14433  psr1clfi  14450  tgidm  14546  tgrest  14641  txbas  14730  reldvg  15151  dvfvalap  15153  bj-indint  15867  bj-nn0suc0  15886  bj-nntrans  15887