Description: Alternate proof of equs5e . Uses ax-12 but not ax-13 . (Contributed by NM, 2-Feb-2007) (Proof shortened by Wolf Lammen, 15-Jan-2018) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | equs5eALT | ⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∃ 𝑦 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfa1 | ⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝑥 = 𝑦 → ∃ 𝑦 𝜑 ) | |
| 2 | hbe1 | ⊢ ( ∃ 𝑦 𝜑 → ∀ 𝑦 ∃ 𝑦 𝜑 ) | |
| 3 | 2 | 19.23bi | ⊢ ( 𝜑 → ∀ 𝑦 ∃ 𝑦 𝜑 ) |
| 4 | ax-12 | ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑦 ∃ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∃ 𝑦 𝜑 ) ) ) | |
| 5 | 3 4 | syl5 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ∃ 𝑦 𝜑 ) ) ) |
| 6 | 5 | imp | ⊢ ( ( 𝑥 = 𝑦 ∧ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∃ 𝑦 𝜑 ) ) |
| 7 | 1 6 | exlimi | ⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ∃ 𝑦 𝜑 ) ) |