Description: The antecedent A. x ( ph -> x = z ) relates to E* x ph , but is better suited for usage in proofs. Note that no distinct variable restriction is placed on ph .
This theorem provides a basic working step in proving theorems about E* or E! . (Contributed by Wolf Lammen, 3-Oct-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-lem-moexsb | |- ( A. x ( ph -> x = z ) -> ( E. x ph <-> [ z / x ] ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfa1 | |- F/ x A. x ( ph -> x = z ) |
|
| 2 | nfs1v | |- F/ x [ z / x ] ph |
|
| 3 | sp | |- ( A. x ( ph -> x = z ) -> ( ph -> x = z ) ) |
|
| 4 | ax12v2 | |- ( x = z -> ( ph -> A. x ( x = z -> ph ) ) ) |
|
| 5 | 3 4 | syli | |- ( A. x ( ph -> x = z ) -> ( ph -> A. x ( x = z -> ph ) ) ) |
| 6 | sb6 | |- ( [ z / x ] ph <-> A. x ( x = z -> ph ) ) |
|
| 7 | 5 6 | syl6ibr | |- ( A. x ( ph -> x = z ) -> ( ph -> [ z / x ] ph ) ) |
| 8 | 1 2 7 | exlimd | |- ( A. x ( ph -> x = z ) -> ( E. x ph -> [ z / x ] ph ) ) |
| 9 | spsbe | |- ( [ z / x ] ph -> E. x ph ) |
|
| 10 | 8 9 | impbid1 | |- ( A. x ( ph -> x = z ) -> ( E. x ph <-> [ z / x ] ph ) ) |