Theorem rgenw 2588

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

Syntax hints:   ∈ wcel 2202  ∀wral 2511

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 2516

This theorem is referenced by:  rgen2w  2589  reuun1  3491  0disj  4090  iinexgm  4249  epse  4445  xpiindim  4873  eliunxp  4875  opeliunxp2  4876  elrnmpti  4991  fnmpti  5468  mpoeq12  6091  relmptopab  6234  iunex  6294  mpoex  6388  opeliunxp2f  6447  ixpssmap  6944  1domsn  7044  nneneq  7086  nqprrnd  7823  nqprdisj  7824  uzf  9819  sum0  12029  fisumcom2  12079  prod0  12226  fprodcom2fi  12267  phisum  12893  sumhashdc  13000  unennn  13098  prdsvallem  13435  prdsval  13436  fczpsrbag  14767  psr1clfi  14789  tgidm  14885  tgrest  14980  txbas  15069  reldvg  15490  dvfvalap  15492  bj-indint  16647  bj-nn0suc0  16666  bj-nntrans  16667