Theorem ax7

Description: Proof of ax-7 from ax7v1 and ax7v2 (and earlier axioms), proving sufficiency of the conjunction of the latter two weakened versions of ax7v , which is itself a weakened version of ax-7 .

Note that the weakened version of ax-7 obtained by adding a disjoint variable condition on x , z (resp. on y , z ) does not permit, together with the other axioms, to prove reflexivity (resp. symmetry). (Contributed by BJ, 7-Dec-2020)

	Ref	Expression
Assertion	ax7	|- ( x = y -> ( x = z -> y = z ) )

Proof

Step	Hyp	Ref	Expression
1		ax7v2	|- ( x = t -> ( x = y -> t = y ) )
2		ax7v2	|- ( x = t -> ( x = z -> t = z ) )
3		ax7v1	|- ( t = y -> ( t = z -> y = z ) )
4	3	imp	|- ( ( t = y /\ t = z ) -> y = z )
5	4	a1i	|- ( x = t -> ( ( t = y /\ t = z ) -> y = z ) )
6	1 2 5	syl2and	|- ( x = t -> ( ( x = y /\ x = z ) -> y = z ) )
7		ax6evr	|- E. t x = t
8	6 7	exlimiiv	|- ( ( x = y /\ x = z ) -> y = z )
9	8	ex	|- ( x = y -> ( x = z -> y = z ) )