Metamath Proof Explorer

Theorem nfsab1OLD

Description: Obsolete version of nfsab1 as of 20-Sep-2023. (Contributed by Mario Carneiro, 11-Aug-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nfsab1OLD 
|- F/ x y e. { x | ph }

Proof

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