Theorem wl-axc11rc11 37537

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

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007

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

This theorem is referenced by: (None)