![]() |
Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-axc11rc11 | Structured version Visualization version GIF version |
Description: Proving axc11r 2365 from axc11 2429. The hypotheses are two instances of
axc11 2429 used in the proof here. Some systems
introduce axc11 2429 as an
axiom, see for example System S2 in
https://us.metamath.org/downloads/finiteaxiom.pdf 2429.
By contrast, this database sees the variant axc11r 2365, directly derived from ax-12 2172, as foundational. Later axc11 2429 is proven somewhat trickily, requiring ax-10 2138 and ax-13 2371, see its proof. (Contributed by Wolf Lammen, 18-Jul-2023.) |
Ref | Expression |
---|---|
wl-axc11rc11.1 | ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥)) |
wl-axc11rc11.2 | ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) |
Ref | Expression |
---|---|
wl-axc11rc11 | ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wl-axc11rc11.1 | . . 3 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥)) | |
2 | 1 | pm2.43i 52 | . 2 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥) |
3 | equcomi 2021 | . . 3 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦) | |
4 | 3 | alimi 1814 | . 2 ⊢ (∀𝑥 𝑦 = 𝑥 → ∀𝑥 𝑥 = 𝑦) |
5 | wl-axc11rc11.2 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | |
6 | 2, 4, 5 | 3syl 18 | 1 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |