Theorem bj-equsal1t

Description: Duplication of wl-equsal1t , with shorter proof. If one imposes a disjoint variable condition on x,y , then one can use alequexv and reduce axiom dependencies, and similarly for the following theorems. Note: wl-equsalcom is also interesting. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-equsal1t	⊢ ( Ⅎ 𝑥 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-alequex	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∃ 𝑥 𝜑 )
2		19.9t	⊢ ( Ⅎ 𝑥 𝜑 → ( ∃ 𝑥 𝜑 ↔ 𝜑 ) )
3	1 2	syl5ib	⊢ ( Ⅎ 𝑥 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → 𝜑 ) )
4		nf5r	⊢ ( Ⅎ 𝑥 𝜑 → ( 𝜑 → ∀ 𝑥 𝜑 ) )
5		ala1	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
6	4 5	syl6	⊢ ( Ⅎ 𝑥 𝜑 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
7	3 6	impbid	⊢ ( Ⅎ 𝑥 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ 𝜑 ) )