Theorem wl-axc11rc11 37627

Description: Proving axc11r 2368 from axc11 2430. The hypotheses are two instances of axc11 2430 used in the proof here. Some systems introduce axc11 2430 as an axiom, see for example System S2 in https://us.metamath.org/downloads/finiteaxiom.pdf 2430.

By contrast, this database sees the variant axc11r 2368, directly derived from ax-12 2180, as foundational. Later axc11 2430 is proven somewhat trickily, requiring ax-10 2144 and ax-13 2372, see its proof. (Contributed by Wolf Lammen, 18-Jul-2023.)

Hypotheses

Ref	Expression
wl-axc11rc11.1	⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥))
wl-axc11rc11.2	⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))

Assertion

Ref	Expression
wl-axc11rc11	⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))

Proof of Theorem wl-axc11rc11

Step	Hyp	Ref	Expression
1		wl-axc11rc11.1	. . 3 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥))
2	1	pm2.43i 52	. 2 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥)
3		equcomi 2018	. . 3 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
4	3	alimi 1812	. 2 ⊢ (∀𝑥 𝑦 = 𝑥 → ∀𝑥 𝑥 = 𝑦)
5		wl-axc11rc11.2	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
6	2, 4, 5	3syl 18	1 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by: (None)