Theorem equvel

Description: A variable elimination law for equality with no distinct variable requirements. Compare equvini . Usage of this theorem is discouraged because it depends on ax-13 . Use equvelv when possible. (Contributed by NM, 1-Mar-2013) (Proof shortened by Mario Carneiro, 17-Oct-2016) (Proof shortened by Wolf Lammen, 15-Jun-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	equvel	⊢ ( ∀ 𝑧 ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑦 ) → 𝑥 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		albi	⊢ ( ∀ 𝑧 ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑦 ) → ( ∀ 𝑧 𝑧 = 𝑥 ↔ ∀ 𝑧 𝑧 = 𝑦 ) )
2		ax6e	⊢ ∃ 𝑧 𝑧 = 𝑦
3		biimpr	⊢ ( ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑦 ) → ( 𝑧 = 𝑦 → 𝑧 = 𝑥 ) )
4		ax7	⊢ ( 𝑧 = 𝑥 → ( 𝑧 = 𝑦 → 𝑥 = 𝑦 ) )
5	3 4	syli	⊢ ( ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑦 ) → ( 𝑧 = 𝑦 → 𝑥 = 𝑦 ) )
6	5	com12	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑦 ) → 𝑥 = 𝑦 ) )
7	2 6	eximii	⊢ ∃ 𝑧 ( ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑦 ) → 𝑥 = 𝑦 )
8	7	19.35i	⊢ ( ∀ 𝑧 ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑦 ) → ∃ 𝑧 𝑥 = 𝑦 )
9	4	spsd	⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑧 𝑧 = 𝑦 → 𝑥 = 𝑦 ) )
10	9	sps	⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑧 𝑧 = 𝑦 → 𝑥 = 𝑦 ) )
11	10	a1dd	⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑧 𝑧 = 𝑦 → ( ∃ 𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦 ) ) )
12		nfeqf	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → Ⅎ 𝑧 𝑥 = 𝑦 )
13	12	19.9d	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( ∃ 𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦 ) )
14	13	ex	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( ∃ 𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦 ) ) )
15	11 14	bija	⊢ ( ( ∀ 𝑧 𝑧 = 𝑥 ↔ ∀ 𝑧 𝑧 = 𝑦 ) → ( ∃ 𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦 ) )
16	1 8 15	sylc	⊢ ( ∀ 𝑧 ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑦 ) → 𝑥 = 𝑦 )