Theorem rgenw 2563

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

Syntax hints:   ∈ wcel 2178  ∀wral 2486

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 1473

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

This theorem is referenced by:  rgen2w  2564  reuun1  3463  0disj  4056  iinexgm  4214  epse  4407  xpiindim  4833  eliunxp  4835  opeliunxp2  4836  elrnmpti  4950  fnmpti  5424  mpoeq12  6028  iunex  6231  mpoex  6323  opeliunxp2f  6347  ixpssmap  6842  1domsn  6939  nneneq  6979  nqprrnd  7691  nqprdisj  7692  uzf  9686  sum0  11814  fisumcom2  11864  prod0  12011  fprodcom2fi  12052  phisum  12678  sumhashdc  12785  unennn  12883  prdsvallem  13219  prdsval  13220  fczpsrbag  14548  psr1clfi  14565  tgidm  14661  tgrest  14756  txbas  14845  reldvg  15266  dvfvalap  15268  bj-indint  16066  bj-nn0suc0  16085  bj-nntrans  16086