Metamath Proof Explorer

Theorem wl-equsalcom

Description: This simple equivalence eases substitution of one expression for the other. (Contributed by Wolf Lammen, 1-Sep-2018)

Ref Expression
Assertion wl-equsalcom 
|- ( A. x ( x = y -> ph ) <-> A. x ( y = x -> ph ) )

Proof

Step Hyp Ref Expression
1 equcom 
 |-  ( x = y <-> y = x )
2 1 imbi1i 
 |-  ( ( x = y -> ph ) <-> ( y = x -> ph ) )
3 2 albii 
 |-  ( A. x ( x = y -> ph ) <-> A. x ( y = x -> ph ) )