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