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\to \left(x=z\to y=z\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax7v2	$$⊢x=t\to \left(x=y\to t=y\right)$$
2		ax7v2	$$⊢x=t\to \left(x=z\to t=z\right)$$
3		ax7v1	$$⊢t=y\to \left(t=z\to y=z\right)$$
4	3	imp	$$⊢\left(t=y\wedge t=z\right)\to y=z$$
5	4	a1i	$$⊢x=t\to \left(\left(t=y\wedge t=z\right)\to y=z\right)$$
6	1 2 5	syl2and	$$⊢x=t\to \left(\left(x=y\wedge x=z\right)\to y=z\right)$$
7		ax6evr	$$⊢\exists tx=t$$
8	6 7	exlimiiv	$$⊢\left(x=y\wedge x=z\right)\to y=z$$
9	8	ex	$$⊢x=y\to \left(x=z\to y=z\right)$$