Theorem rgenw 2487

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

Syntax hints:   ∈ wcel 1480  ∀wral 2416

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 1425

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

This theorem is referenced by:  rgen2w  2488  reuun1  3358  0disj  3926  iinexgm  4079  epse  4264  xpiindim  4676  eliunxp  4678  opeliunxp2  4679  elrnmpti  4792  fnmpti  5251  mpoeq12  5831  iunex  6021  mpoex  6111  opeliunxp2f  6135  ixpssmap  6626  1domsn  6713  nneneq  6751  nqprrnd  7351  nqprdisj  7352  uzf  9329  sum0  11157  fisumcom2  11207  unennn  11910  tgidm  12243  tgrest  12338  txbas  12427  reldvg  12817  dvfvalap  12819  bj-indint  13129  bj-nn0suc0  13148  bj-nntrans  13149