# 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 syl5bi
` |-  ( ( -. 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 ) )`