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  6081  relmptopab  6224  iunex  6285  mpoex  6379  opeliunxp2f  6404  ixpssmap  6901  1domsn  7001  nneneq  7043  nqprrnd  7763  nqprdisj  7764  uzf  9758  sum0  11967  fisumcom2  12017  prod0  12164  fprodcom2fi  12205  phisum  12831  sumhashdc  12938  unennn  13036  prdsvallem  13373  prdsval  13374  fczpsrbag  14704  psr1clfi  14721  tgidm  14817  tgrest  14912  txbas  15001  reldvg  15422  dvfvalap  15424  bj-indint  16577  bj-nn0suc0  16596  bj-nntrans  16597