Metamath Proof Explorer

Theorem hbab1OLD

Description: Obsolete version of hbab1 as of 25-Oct-2024. (Contributed by NM, 26-May-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion hbab1OLD 
|- ( 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 } )