Metamath Proof Explorer


Theorem ax12

Description: Rederivation of Axiom ax-12 from ax12v (used only via sp ) , axc11r , and axc15 (on top of Tarski's FOL). Since this version depends on ax-13 , usage of the weaker ax12v , ax12w , ax12i are preferred. (Contributed by NM, 22-Jan-2007) Proof uses contemporary axioms. (Revised by Wolf Lammen, 8-Aug-2020) (Proof shortened by BJ, 4-Jul-2021) (New usage is discouraged.)

Ref Expression
Assertion ax12
|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )

Proof

Step Hyp Ref Expression
1 axc11r
 |-  ( A. x x = y -> ( A. y ph -> A. x ph ) )
2 ala1
 |-  ( A. x ph -> A. x ( x = y -> ph ) )
3 1 2 syl6
 |-  ( A. x x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
4 3 a1d
 |-  ( A. x x = y -> ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) ) )
5 sp
 |-  ( A. y ph -> ph )
6 axc15
 |-  ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
7 5 6 syl7
 |-  ( -. A. x x = y -> ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) ) )
8 4 7 pm2.61i
 |-  ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )