Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-axc11rc11 Structured version   Visualization version   GIF version

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

By contrast, this database sees the variant axc11r 2369, directly derived from ax-12 2179, as foundational. Later axc11 2431 is proven somewhat trickily, requiring ax-10 2145 and ax-13 2373, 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
StepHypRef Expression
1 wl-axc11rc11.1 . . 3 (∀𝑦 𝑦 = 𝑥 → (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥))
21pm2.43i 52 . 2 (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥)
3 equcomi 2029 . . 3 (𝑦 = 𝑥𝑥 = 𝑦)
43alimi 1818 . 2 (∀𝑥 𝑦 = 𝑥 → ∀𝑥 𝑥 = 𝑦)
5 wl-axc11rc11.2 . 2 (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
62, 4, 53syl 18 1 (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator