Metamath Proof Explorer

Theorem rgenw

Description: Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014)

Ref Expression
Hypothesis rgenw.1 
|- ph
Assertion rgenw 
|- A. x e. A ph

Proof

Step Hyp Ref Expression
1 rgenw.1 
 |-  ph
2 1 a1i 
 |-  ( x e. A -> ph )
3 2 rgen 
 |-  A. x e. A ph