Theorem rgenw 2605

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

This proof depends on syntax axioms:   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  rgen2w  2606  reuun1  3515  0disj  4127  iinexgm  4290  epse  4487  xpiindim  4917  eliunxp  4919  opeliunxp2  4920  elrnmpti  5035  fnmpti  5512  mpoeq12  6148  relmptopab  6291  iunex  6352  mpoex  6450  opeliunxp2f  6509  ixpssmap  7014  1domsn  7115  nneneq  7158  nqprrnd  7910  nqprdisj  7911  uzf  9933  hashfibclem  11296  sum0  12171  fisumcom2  12221  prod0  12368  fprodcom2fi  12409  phisum  13039  sumhashdc  13146  unennn  13337  prdsvallem  13670  prdsval  14222  fczpsrbag  15105  psr1clfi  15128  tgidm  15224  tgrest  15319  txbas  15408  reldvg  15829  dvfvalap  15831  bj-indint  17055  bj-nn0suc0  17074  bj-nntrans  17075