Description: One direction of a simplified definition of substitution when variables are distinct. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 5-Aug-1993) (Proof shortened by Wolf Lammen, 21-Feb-2024) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sb3 | |- ( -. A. x x = y -> ( E. x ( x = y /\ ph ) -> [ y / x ] ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sb3b | |- ( -. A. x x = y -> ( [ y / x ] ph <-> E. x ( x = y /\ ph ) ) ) |
|
| 2 | 1 | biimprd | |- ( -. A. x x = y -> ( E. x ( x = y /\ ph ) -> [ y / x ] ph ) ) |