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	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		ax7v2	⊢ ( 𝑥 = 𝑡 → ( 𝑥 = 𝑦 → 𝑡 = 𝑦 ) )
2		ax7v2	⊢ ( 𝑥 = 𝑡 → ( 𝑥 = 𝑧 → 𝑡 = 𝑧 ) )
3		ax7v1	⊢ ( 𝑡 = 𝑦 → ( 𝑡 = 𝑧 → 𝑦 = 𝑧 ) )
4	3	imp	⊢ ( ( 𝑡 = 𝑦 ∧ 𝑡 = 𝑧 ) → 𝑦 = 𝑧 )
5	4	a1i	⊢ ( 𝑥 = 𝑡 → ( ( 𝑡 = 𝑦 ∧ 𝑡 = 𝑧 ) → 𝑦 = 𝑧 ) )
6	1 2 5	syl2and	⊢ ( 𝑥 = 𝑡 → ( ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑧 ) → 𝑦 = 𝑧 ) )
7		ax6evr	⊢ ∃ 𝑡 𝑥 = 𝑡
8	6 7	exlimiiv	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑧 ) → 𝑦 = 𝑧 )
9	8	ex	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) )