Theorem wl-axc11rc11 37606

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

By contrast, this database sees the variant axc11r 2371, directly derived from ax-12 2178, as foundational. Later axc11 2435 is proven somewhat trickily, requiring ax-10 2142 and ax-13 2377, 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 2017	. . 3 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
4	3	alimi 1811	. 2 ⊢ (∀𝑥 𝑦 = 𝑥 → ∀𝑥 𝑥 = 𝑦)
5		wl-axc11rc11.2	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
6	2, 4, 5	3syl 18	1 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

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

This theorem is referenced by: (None)