Theorem rgenw 2525

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

Syntax hints:   ∈ wcel 2141  ∀wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1442

This theorem depends on definitions:  df-bi 116  df-ral 2453

This theorem is referenced by:  rgen2w  2526  reuun1  3409  0disj  3986  iinexgm  4140  epse  4327  xpiindim  4748  eliunxp  4750  opeliunxp2  4751  elrnmpti  4864  fnmpti  5326  mpoeq12  5913  iunex  6102  mpoex  6193  opeliunxp2f  6217  ixpssmap  6710  1domsn  6797  nneneq  6835  nqprrnd  7505  nqprdisj  7506  uzf  9490  sum0  11351  fisumcom2  11401  prod0  11548  fprodcom2fi  11589  phisum  12194  sumhashdc  12299  unennn  12352  tgidm  12868  tgrest  12963  txbas  13052  reldvg  13442  dvfvalap  13444  bj-indint  13966  bj-nn0suc0  13985  bj-nntrans  13986