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 | |- ( A. x ( x = y -> ph ) <-> ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.23v | |- ( A. x ( x = y -> ph ) <-> ( E. x x = y -> ph ) ) |
|
| 2 | ax6ev | |- E. x x = y |
|
| 3 | 2 | a1bi | |- ( ph <-> ( E. x x = y -> ph ) ) |
| 4 | 1 3 | bitr4i | |- ( A. x ( x = y -> ph ) <-> ph ) |