Theorem wl-euequf

Description: euequ proved with a distinctor. (Contributed by Wolf Lammen, 23-Sep-2020)

	Ref	Expression
Assertion	wl-euequf	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃! 𝑥 𝑥 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		ax6ev	⊢ ∃ 𝑧 𝑧 = 𝑦
2		nfv	⊢ Ⅎ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦
3		nfna1	⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
4		nfeqf2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑧 = 𝑦 )
5		equequ2	⊢ ( 𝑦 = 𝑧 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) )
6	5	equcoms	⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) )
7	6	a1i	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) ) )
8	3 4 7	alrimdd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) ) )
9	2 8	eximd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑧 𝑧 = 𝑦 → ∃ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) ) )
10	1 9	mpi	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) )
11		eu6	⊢ ( ∃! 𝑥 𝑥 = 𝑦 ↔ ∃ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) )
12	10 11	sylibr	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃! 𝑥 𝑥 = 𝑦 )