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  4128  iinexgm  4292  epse  4489  xpiindim  4919  eliunxp  4921  opeliunxp2  4922  elrnmpti  5037  fnmpti  5515  mpoeq12  6151  relmptopab  6294  iunex  6356  mpoex  6454  opeliunxp2f  6513  ixpssmap  7018  1domsn  7119  nneneq  7162  nqprrnd  7916  nqprdisj  7917  uzf  9940  hashfibclem  11304  sum0  12180  fisumcom2  12230  prod0  12377  fprodcom2fi  12418  phisum  13048  sumhashdc  13155  unennn  13346  prdsvallem  13680  gsum2d2fi  14274  gsumcom2fi  14275  prdsval  14280  fczpsrbag  15165  psr1clfi  15198  tgidm  15300  tgrest  15395  txbas  15484  reldvg  15905  dvfvalap  15907  bj-indint  17162  bj-nn0suc0  17181  bj-nntrans  17182