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  9924  hashfibclem  11282  sum0  12155  fisumcom2  12205  prod0  12352  fprodcom2fi  12393  phisum  13019  sumhashdc  13126  unennn  13288  prdsvallem  13621  prdsval  14173  fczpsrbag  15056  psr1clfi  15079  tgidm  15175  tgrest  15270  txbas  15359  reldvg  15780  dvfvalap  15782  bj-indint  16957  bj-nn0suc0  16976  bj-nntrans  16977