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

Proof

Step	Hyp	Ref	Expression
1		equtr	$⊢ z = x \to (x = y \to z = y)$
2		equcomi	$⊢ z = x \to x = z$
3	1 2	jctild	$⊢ z = x \to (x = y \to (x = z \land z = y))$
4		19.8a	$⊢ (x = z \land z = y) \to \exists z (x = z \land z = y)$
5	3 4	syl6	$⊢ z = x \to (x = y \to \exists z (x = z \land z = y))$
6		ax13	$⊢ \neg z = x \to (x = y \to \forall z x = y)$
7		ax6e	$⊢ \exists z z = x$
8	7 3	eximii	$⊢ \exists z (x = y \to (x = z \land z = y))$
9	8	19.35i	$⊢ \forall z x = y \to \exists z (x = z \land z = y)$
10	6 9	syl6	$⊢ \neg z = x \to (x = y \to \exists z (x = z \land z = y))$
11	5 10	pm2.61i	$⊢ x = y \to \exists z (x = z \land z = y)$

Metamath Proof Explorer

Theorem equvini

Proof