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  7627  nqprdisj  7628  uzf  9621  sum0  11570  fisumcom2  11620  prod0  11767  fprodcom2fi  11808  phisum  12434  sumhashdc  12541  unennn  12639  prdsvallem  12974  prdsval  12975  fczpsrbag  14301  psr1clfi  14316  tgidm  14394  tgrest  14489  txbas  14578  reldvg  14999  dvfvalap  15001  bj-indint  15661  bj-nn0suc0  15680  bj-nntrans  15681