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 36064
Description: Proving axc11r 2365 from axc11 2429. The hypotheses are two instances of axc11 2429 used in the proof here. Some systems introduce axc11 2429 as an axiom, see for example System S2 in https://us.metamath.org/downloads/finiteaxiom.pdf 2429.

By contrast, this database sees the variant axc11r 2365, directly derived from ax-12 2172, as foundational. Later axc11 2429 is proven somewhat trickily, requiring ax-10 2138 and ax-13 2371, 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 2021 . . 3 (𝑦 = 𝑥𝑥 = 𝑦)
43alimi 1814 . 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator