Metamath Proof Explorer

Theorem hbab1

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 26-May-1993)

Ref Expression
Assertion hbab1 
|- ( y e. { x | ph } -> A. x y e. { x | ph } )

Proof

Step Hyp Ref Expression
1 df-clab 
 |-  ( y e. { x | ph } <-> [ y / x ] ph )
2 hbs1 
 |-  ( [ y / x ] ph -> A. x [ y / x ] ph )
3 1 2 hbxfrbi 
 |-  ( y e. { x | ph } -> A. x y e. { x | ph } )