Theorem wl-aleq

Description: The semantics of A. x y = z . (Contributed by Wolf Lammen, 27-Apr-2018)

	Ref	Expression
Assertion	wl-aleq	⊢ ( ∀ 𝑥 𝑦 = 𝑧 ↔ ( 𝑦 = 𝑧 ∧ ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sp	⊢ ( ∀ 𝑥 𝑦 = 𝑧 → 𝑦 = 𝑧 )
2		equequ2	⊢ ( 𝑦 = 𝑧 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) )
3	2	alimi	⊢ ( ∀ 𝑥 𝑦 = 𝑧 → ∀ 𝑥 ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) )
4		albi	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) → ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) )
5	3 4	syl	⊢ ( ∀ 𝑥 𝑦 = 𝑧 → ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) )
6	1 5	jca	⊢ ( ∀ 𝑥 𝑦 = 𝑧 → ( 𝑦 = 𝑧 ∧ ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) ) )
7		ax7	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) )
8	7	al2imi	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )
9	8	a1dd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) )
10		axc9	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) )
11	9 10	bija	⊢ ( ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )
12	11	impcom	⊢ ( ( 𝑦 = 𝑧 ∧ ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) ) → ∀ 𝑥 𝑦 = 𝑧 )
13	6 12	impbii	⊢ ( ∀ 𝑥 𝑦 = 𝑧 ↔ ( 𝑦 = 𝑧 ∧ ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 𝑥 = 𝑧 ) ) )