Metamath Proof Explorer

Theorem alral

Description: Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006)

Ref Expression
Assertion alral 
|- ( A. x ph -> A. x e. A ph )

Proof

Step Hyp Ref Expression
1 ala1 
 |-  ( A. x ph -> A. x ( x e. A -> ph ) )
2 df-ral 
 |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
3 1 2 sylibr 
 |-  ( A. x ph -> A. x e. A ph )