Metamath Proof Explorer

Theorem hbab1

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 26-May-1993) (Proof shortened by Wolf Lammen, 25-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 nfsab1 
 |-  F/ x y e. { x | ph }
2 1 nf5ri 
 |-  ( y e. { x | ph } -> A. x y e. { x | ph } )