Description: Simplified definition of substitution when variables are distinct. This is the biconditional strengthening of sb3 . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BJ, 6-Oct-2018) Shorten sb3 . (Revised by Wolf Lammen, 21-Feb-2021) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sb3b | |- ( -. A. x x = y -> ( [ y / x ] ph <-> E. x ( x = y /\ ph ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sb4b | |- ( -. A. x x = y -> ( [ y / x ] ph <-> A. x ( x = y -> ph ) ) ) |
|
| 2 | equs5 | |- ( -. A. x x = y -> ( E. x ( x = y /\ ph ) <-> A. x ( x = y -> ph ) ) ) |
|
| 3 | 1 2 | bitr4d | |- ( -. A. x x = y -> ( [ y / x ] ph <-> E. x ( x = y /\ ph ) ) ) |