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  6514  ixpssmap  7020  1domsn  7121  nneneq  7164  nqprrnd  7916  nqprdisj  7917  uzf  9939  hashfibclem  11303  sum0  12179  fisumcom2  12229  prod0  12376  fprodcom2fi  12417  phisum  13047  sumhashdc  13154  unennn  13345  prdsvallem  13679  gsum2d2fi  14273  gsumcom2fi  14274  prdsval  14279  fczpsrbag  15169  psr1clfi  15207  tgidm  15317  tgrest  15412  txbas  15501  reldvg  15922  dvfvalap  15924  bj-indint  17179  bj-nn0suc0  17198  bj-nntrans  17199