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 } ) |
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 } ) |