Theorem wl-axc11rc11 38034

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

By contrast, this database sees the variant axc11r 2393, directly derived from ax-12 2206, as foundational. Later axc11 2455 is proven somewhat trickily, requiring ax-10 2169 and ax-13 2397, 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 2031	. . 3 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
4	3	alimi 1825	. 2 ⊢ (∀𝑥 𝑦 = 𝑥 → ∀𝑥 𝑥 = 𝑦)
5		wl-axc11rc11.2	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
6	2, 4, 5	3syl 18	1 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))

Syntax hints:   → wi 4  ∀wal 1552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1794

This theorem is referenced by: (None)