# Metamath Proof Explorer

## 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 {t}\phantom{\rule{.4em}{0ex}}{x}={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)$