Metamath Proof Explorer

Theorem sb6a

Description: Equivalence for substitution. (Contributed by NM, 2-Jun-1993) (Proof shortened by Wolf Lammen, 23-Sep-2018)

Ref Expression
Assertion sb6a 
|- ( [ y / x ] ph <-> A. x ( x = y -> [ x / y ] ph ) )

Proof

Step Hyp Ref Expression
1 sbcov 
 |-  ( [ y / x ] [ x / y ] ph <-> [ y / x ] ph )
2 sb6 
 |-  ( [ y / x ] [ x / y ] ph <-> A. x ( x = y -> [ x / y ] ph ) )
3 1 2 bitr3i 
 |-  ( [ y / x ] ph <-> A. x ( x = y -> [ x / y ] ph ) )