Metamath Proof Explorer


Theorem wl-axc11rc11

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

Proof

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