Metamath Proof Explorer

Theorem equsv

Description: If a formula does not contain a variable x , then it is equivalent to the corresponding prototype of substitution with a fresh variable (see sb6 ). (Contributed by BJ, 23-Jul-2023)

Ref Expression
Assertion equsv x x = y φ φ


Step Hyp Ref Expression
1 19.23v x x = y φ x x = y φ
2 ax6ev x x = y
3 2 a1bi φ x x = y φ
4 1 3 bitr4i x x = y φ φ