Theorem rgenw 2597

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

Syntax hints:   ∈ wcel 2203  ∀wral 2520

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 1498

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

This theorem is referenced by:  rgen2w  2598  reuun1  3503  0disj  4106  iinexgm  4266  epse  4463  xpiindim  4892  eliunxp  4894  opeliunxp2  4895  elrnmpti  5010  fnmpti  5487  mpoeq12  6113  relmptopab  6256  iunex  6316  mpoex  6410  opeliunxp2f  6469  ixpssmap  6967  1domsn  7068  nneneq  7111  nqprrnd  7858  nqprdisj  7859  uzf  9856  hashfibclem  11206  sum0  12074  fisumcom2  12124  prod0  12271  fprodcom2fi  12312  phisum  12938  sumhashdc  13045  unennn  13148  prdsvallem  13485  prdsval  13486  fczpsrbag  14820  psr1clfi  14843  tgidm  14939  tgrest  15034  txbas  15123  reldvg  15544  dvfvalap  15546  bj-indint  16701  bj-nn0suc0  16720  bj-nntrans  16721