Theorem wl-axc11rc11 38204

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

By contrast, this database sees the variant axc11r 2398, directly derived from ax-12 2211, as foundational. Later axc11 2460 is proven somewhat trickily, requiring ax-10 2174 and ax-13 2402, 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 53	. 2 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥)
3		equcomi 2045	. . 3 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
4	3	alimi 1839	. 2 ⊢ (∀𝑥 𝑦 = 𝑥 → ∀𝑥 𝑥 = 𝑦)
5		wl-axc11rc11.2	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
6	2, 4, 5	3syl 19	1 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))

Syntax hints:   → wi 4  ∀wal 1566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808

This theorem is referenced by: (None)