Theorem rgenw 2552

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

Syntax hints:   ∈ wcel 2167  ∀wral 2475

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 1463

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

This theorem is referenced by:  rgen2w  2553  reuun1  3446  0disj  4031  iinexgm  4188  epse  4378  xpiindim  4804  eliunxp  4806  opeliunxp2  4807  elrnmpti  4920  fnmpti  5389  mpoeq12  5986  iunex  6189  mpoex  6281  opeliunxp2f  6305  ixpssmap  6800  1domsn  6887  nneneq  6927  nqprrnd  7629  nqprdisj  7630  uzf  9623  sum0  11572  fisumcom2  11622  prod0  11769  fprodcom2fi  11810  phisum  12436  sumhashdc  12543  unennn  12641  prdsvallem  12976  prdsval  12977  fczpsrbag  14305  psr1clfi  14322  tgidm  14418  tgrest  14513  txbas  14602  reldvg  15023  dvfvalap  15025  bj-indint  15685  bj-nn0suc0  15704  bj-nntrans  15705