Theorem wl-equsal1i

Description: The antecedent x = y is irrelevant, if one or both setvar variables are not free in ph . (Contributed by Wolf Lammen, 1-Sep-2018)

	Ref	Expression
Hypotheses	wl-equsal1i.1	⊢ ( Ⅎ 𝑥 𝜑 ∨ Ⅎ 𝑦 𝜑 )
	wl-equsal1i.2	⊢ ( 𝑥 = 𝑦 → 𝜑 )
Assertion	wl-equsal1i	⊢ 𝜑

Proof

Step	Hyp	Ref	Expression
1		wl-equsal1i.1	⊢ ( Ⅎ 𝑥 𝜑 ∨ Ⅎ 𝑦 𝜑 )
2		wl-equsal1i.2	⊢ ( 𝑥 = 𝑦 → 𝜑 )
3	2	gen2	⊢ ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 )
4		sp	⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
5	4	alcoms	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
6		wl-equsal1t	⊢ ( Ⅎ 𝑥 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ 𝜑 ) )
7	5 6	imbitrid	⊢ ( Ⅎ 𝑥 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 ) → 𝜑 ) )
8		wl-equsalcom	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) ↔ ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 ) )
9		wl-equsal1t	⊢ ( Ⅎ 𝑦 𝜑 → ( ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) ↔ 𝜑 ) )
10	9	biimpd	⊢ ( Ⅎ 𝑦 𝜑 → ( ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) → 𝜑 ) )
11	8 10	biimtrrid	⊢ ( Ⅎ 𝑦 𝜑 → ( ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 ) → 𝜑 ) )
12	11	spsd	⊢ ( Ⅎ 𝑦 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 ) → 𝜑 ) )
13	7 12	jaoi	⊢ ( ( Ⅎ 𝑥 𝜑 ∨ Ⅎ 𝑦 𝜑 ) → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 ) → 𝜑 ) )
14	1 3 13	mp2	⊢ 𝜑