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

Proof

Step	Hyp	Ref	Expression
1		equtr	⊢ ( 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → 𝑧 = 𝑦 ) )
2		equcomi	⊢ ( 𝑧 = 𝑥 → 𝑥 = 𝑧 )
3	1 2	jctild	⊢ ( 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) ) )
4		19.8a	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) )
5	3 4	syl6	⊢ ( 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) ) )
6		ax13	⊢ ( ¬ 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) )
7		ax6e	⊢ ∃ 𝑧 𝑧 = 𝑥
8	7 3	eximii	⊢ ∃ 𝑧 ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) )
9	8	19.35i	⊢ ( ∀ 𝑧 𝑥 = 𝑦 → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) )
10	6 9	syl6	⊢ ( ¬ 𝑧 = 𝑥 → ( 𝑥 = 𝑦 → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) ) )
11	5 10	pm2.61i	⊢ ( 𝑥 = 𝑦 → ∃ 𝑧 ( 𝑥 = 𝑧 ∧ 𝑧 = 𝑦 ) )