Theorem rgenw 2587

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

Syntax hints:   ∈ wcel 2202  ∀wral 2510

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 1497

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

This theorem is referenced by:  rgen2w  2588  reuun1  3489  0disj  4085  iinexgm  4244  epse  4439  xpiindim  4867  eliunxp  4869  opeliunxp2  4870  elrnmpti  4985  fnmpti  5461  mpoeq12  6080  relmptopab  6223  iunex  6284  mpoex  6378  opeliunxp2f  6403  ixpssmap  6900  1domsn  7000  nneneq  7042  nqprrnd  7762  nqprdisj  7763  uzf  9757  sum0  11948  fisumcom2  11998  prod0  12145  fprodcom2fi  12186  phisum  12812  sumhashdc  12919  unennn  13017  prdsvallem  13354  prdsval  13355  fczpsrbag  14684  psr1clfi  14701  tgidm  14797  tgrest  14892  txbas  14981  reldvg  15402  dvfvalap  15404  bj-indint  16526  bj-nn0suc0  16545  bj-nntrans  16546