Theorem rgenw 2512

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

Syntax hints:   ∈ wcel 2128  ∀wral 2435

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 1429

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

This theorem is referenced by:  rgen2w  2513  reuun1  3389  0disj  3962  iinexgm  4115  epse  4302  xpiindim  4722  eliunxp  4724  opeliunxp2  4725  elrnmpti  4838  fnmpti  5297  mpoeq12  5878  iunex  6068  mpoex  6158  opeliunxp2f  6182  ixpssmap  6674  1domsn  6761  nneneq  6799  nqprrnd  7457  nqprdisj  7458  uzf  9436  sum0  11278  fisumcom2  11328  prod0  11475  fprodcom2fi  11516  phisum  12103  unennn  12109  tgidm  12445  tgrest  12540  txbas  12629  reldvg  13019  dvfvalap  13021  bj-indint  13477  bj-nn0suc0  13496  bj-nntrans  13497