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 ) ) |