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 | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ( ∃ 𝑥 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfa1 | ⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) | |
| 2 | nfs1v | ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑 | |
| 3 | sp | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ( 𝜑 → 𝑥 = 𝑧 ) ) | |
| 4 | ax12v2 | ⊢ ( 𝑥 = 𝑧 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) | |
| 5 | 3 4 | syli | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) |
| 6 | sb6 | ⊢ ( [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) | |
| 7 | 5 6 | syl6ibr | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ( 𝜑 → [ 𝑧 / 𝑥 ] 𝜑 ) ) |
| 8 | 1 2 7 | exlimd | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ( ∃ 𝑥 𝜑 → [ 𝑧 / 𝑥 ] 𝜑 ) ) |
| 9 | spsbe | ⊢ ( [ 𝑧 / 𝑥 ] 𝜑 → ∃ 𝑥 𝜑 ) | |
| 10 | 8 9 | impbid1 | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ( ∃ 𝑥 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) ) |