Theorem rgenw 2549

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

Syntax hints:   ∈ wcel 2164  ∀wral 2472

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 1460

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

This theorem is referenced by:  rgen2w  2550  reuun1  3442  0disj  4027  iinexgm  4184  epse  4374  xpiindim  4800  eliunxp  4802  opeliunxp2  4803  elrnmpti  4916  fnmpti  5383  mpoeq12  5979  iunex  6177  mpoex  6269  opeliunxp2f  6293  ixpssmap  6788  1domsn  6875  nneneq  6915  nqprrnd  7605  nqprdisj  7606  uzf  9598  sum0  11534  fisumcom2  11584  prod0  11731  fprodcom2fi  11772  phisum  12381  sumhashdc  12488  unennn  12557  fczpsrbag  14168  tgidm  14253  tgrest  14348  txbas  14437  reldvg  14858  dvfvalap  14860  bj-indint  15493  bj-nn0suc0  15512  bj-nntrans  15513