Description: Proving axc11r from axc11 . The hypotheses are two instances of axc11 used in the proof here. Some systems introduce axc11 as an axiom, see for example System S2 in https://us.metamath.org/downloads/finiteaxiom.pdf .
By contrast, this database sees the variant axc11r , directly derived from ax-12 , as foundational. Later axc11 is proven somewhat trickily, requiring ax-10 and ax-13 , see its proof. (Contributed by Wolf Lammen, 18-Jul-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | wl-axc11rc11.1 | ⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∀ 𝑦 𝑦 = 𝑥 → ∀ 𝑥 𝑦 = 𝑥 ) ) | |
| wl-axc11rc11.2 | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜑 ) ) | ||
| Assertion | wl-axc11rc11 | ⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wl-axc11rc11.1 | ⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∀ 𝑦 𝑦 = 𝑥 → ∀ 𝑥 𝑦 = 𝑥 ) ) | |
| 2 | wl-axc11rc11.2 | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜑 ) ) | |
| 3 | 1 | pm2.43i | ⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ∀ 𝑥 𝑦 = 𝑥 ) |
| 4 | equcomi | ⊢ ( 𝑦 = 𝑥 → 𝑥 = 𝑦 ) | |
| 5 | 4 | alimi | ⊢ ( ∀ 𝑥 𝑦 = 𝑥 → ∀ 𝑥 𝑥 = 𝑦 ) |
| 6 | 3 5 2 | 3syl | ⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜑 ) ) |