Theorem rgenw 2532

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

Syntax hints:   ∈ wcel 2148  ∀wral 2455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1449

This theorem depends on definitions:  df-bi 117  df-ral 2460

This theorem is referenced by:  rgen2w  2533  reuun1  3417  0disj  4000  iinexgm  4154  epse  4342  xpiindim  4764  eliunxp  4766  opeliunxp2  4767  elrnmpti  4880  fnmpti  5344  mpoeq12  5934  iunex  6123  mpoex  6214  opeliunxp2f  6238  ixpssmap  6731  1domsn  6818  nneneq  6856  nqprrnd  7541  nqprdisj  7542  uzf  9530  sum0  11395  fisumcom2  11445  prod0  11592  fprodcom2fi  11633  phisum  12239  sumhashdc  12344  unennn  12397  tgidm  13544  tgrest  13639  txbas  13728  reldvg  14118  dvfvalap  14120  bj-indint  14653  bj-nn0suc0  14672  bj-nntrans  14673