# Metamath Proof Explorer

## Theorem equvini

Description: A variable introduction law for equality. Lemma 15 of Monk2 p. 109, however we do not require z to be distinct from x and y . Usage of this theorem is discouraged because it depends on ax-13 . See equvinv for a shorter proof requiring fewer axioms when z is required to be distinct from x and y . (Contributed by NM, 10-Jan-1993) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 16-Sep-2023) (New usage is discouraged.)

Ref Expression
Assertion equvini ${⊢}{x}={y}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({x}={z}\wedge {z}={y}\right)$

### Proof

Step Hyp Ref Expression
1 equtr ${⊢}{z}={x}\to \left({x}={y}\to {z}={y}\right)$
2 equcomi ${⊢}{z}={x}\to {x}={z}$
3 1 2 jctild ${⊢}{z}={x}\to \left({x}={y}\to \left({x}={z}\wedge {z}={y}\right)\right)$
4 19.8a ${⊢}\left({x}={z}\wedge {z}={y}\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({x}={z}\wedge {z}={y}\right)$
5 3 4 syl6 ${⊢}{z}={x}\to \left({x}={y}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({x}={z}\wedge {z}={y}\right)\right)$
6 ax13 ${⊢}¬{z}={x}\to \left({x}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
7 ax6e ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}{z}={x}$
8 7 3 eximii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({x}={z}\wedge {z}={y}\right)\right)$
9 8 19.35i ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}{x}={y}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({x}={z}\wedge {z}={y}\right)$
10 6 9 syl6 ${⊢}¬{z}={x}\to \left({x}={y}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({x}={z}\wedge {z}={y}\right)\right)$
11 5 10 pm2.61i ${⊢}{x}={y}\to \exists {z}\phantom{\rule{.4em}{0ex}}\left({x}={z}\wedge {z}={y}\right)$