Description: Proving axc11r from axc11 . The hypotheses are two instances of axc11 used in the proof here. Some systems introduce axc11 as an axiom, see for example System S2 in https://us.metamath.org/downloads/finiteaxiom.pdf .
By contrast, this database sees the variant axc11r , directly derived from ax-12 , as foundational. Later axc11 is proven somewhat trickily, requiring ax-10 and ax-13 , see its proof. (Contributed by Wolf Lammen, 18-Jul-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | wl-axc11rc11.1 | |- ( A. y y = x -> ( A. y y = x -> A. x y = x ) ) |
|
| wl-axc11rc11.2 | |- ( A. x x = y -> ( A. x ph -> A. y ph ) ) |
||
| Assertion | wl-axc11rc11 | |- ( A. y y = x -> ( A. x ph -> A. y ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wl-axc11rc11.1 | |- ( A. y y = x -> ( A. y y = x -> A. x y = x ) ) |
|
| 2 | wl-axc11rc11.2 | |- ( A. x x = y -> ( A. x ph -> A. y ph ) ) |
|
| 3 | 1 | pm2.43i | |- ( A. y y = x -> A. x y = x ) |
| 4 | equcomi | |- ( y = x -> x = y ) |
|
| 5 | 4 | alimi | |- ( A. x y = x -> A. x x = y ) |
| 6 | 3 5 2 | 3syl | |- ( A. y y = x -> ( A. x ph -> A. y ph ) ) |