Description: The expression x = y in antecedent position plays an important role in predicate logic, namely in implicit substitution. However, occasionally it is irrelevant, and can safely be dropped. A sufficient condition for this is when x (or y or both) is not free in ph .
This theorem is more fundamental than equsal , spimt or sbft , to which it is related. (Contributed by Wolf Lammen, 19-Aug-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-equsal1t | |- ( F/ x ph -> ( A. x ( x = y -> ph ) <-> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfnf1 | |- F/ x F/ x ph |
|
| 2 | id | |- ( F/ x ph -> F/ x ph ) |
|
| 3 | biid | |- ( ph <-> ph ) |
|
| 4 | 3 | 2a1i | |- ( F/ x ph -> ( x = y -> ( ph <-> ph ) ) ) |
| 5 | 1 2 4 | wl-equsald | |- ( F/ x ph -> ( A. x ( x = y -> ph ) <-> ph ) ) |