This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ax13

Description: Derive ax-13 from ax13v and Tarski's FOL. This shows that the weakening in ax13v is still sufficient for a complete system. Preferably, use the weaker ax13w to avoid the propagation of ax-13 . (Contributed by NM, 21-Dec-2015) (Proof shortened by Wolf Lammen, 31-Jan-2018) Reduce axiom usage. (Revised by Wolf Lammen, 2-Jun-2021) (New usage is discouraged.)

Ref Expression
Assertion ax13 
|- ( -. x = y -> ( y = z -> A. x y = z ) )

Proof

Step Hyp Ref Expression
1 equvinv 
 |-  ( y = z <-> E. w ( w = y /\ w = z ) )
2 ax13lem1 
 |-  ( -. x = y -> ( w = y -> A. x w = y ) )
3 2 imp 
 |-  ( ( -. x = y /\ w = y ) -> A. x w = y )
4 ax13lem1 
 |-  ( -. x = z -> ( w = z -> A. x w = z ) )
5 4 imp 
 |-  ( ( -. x = z /\ w = z ) -> A. x w = z )
6 ax7v1 
 |-  ( w = y -> ( w = z -> y = z ) )
7 6 imp 
 |-  ( ( w = y /\ w = z ) -> y = z )
8 7 alanimi 
 |-  ( ( A. x w = y /\ A. x w = z ) -> A. x y = z )
9 3 5 8 syl2an 
 |-  ( ( ( -. x = y /\ w = y ) /\ ( -. x = z /\ w = z ) ) -> A. x y = z )
10 9 an4s 
 |-  ( ( ( -. x = y /\ -. x = z ) /\ ( w = y /\ w = z ) ) -> A. x y = z )
11 10 ex 
 |-  ( ( -. x = y /\ -. x = z ) -> ( ( w = y /\ w = z ) -> A. x y = z ) )
12 11 exlimdv 
 |-  ( ( -. x = y /\ -. x = z ) -> ( E. w ( w = y /\ w = z ) -> A. x y = z ) )
13 1 12 biimtrid 
 |-  ( ( -. x = y /\ -. x = z ) -> ( y = z -> A. x y = z ) )
14 13 ex 
 |-  ( -. x = y -> ( -. x = z -> ( y = z -> A. x y = z ) ) )
15 ax13b 
 |-  ( ( -. x = y -> ( y = z -> A. x y = z ) ) <-> ( -. x = y -> ( -. x = z -> ( y = z -> A. x y = z ) ) ) )
16 14 15 mpbir 
 |-  ( -. x = y -> ( y = z -> A. x y = z ) )