Theorem wl-sb9v

Description: Commutation of quantification and substitution variables based on fewer axioms than sb9 . (Contributed by Wolf Lammen, 27-Apr-2025)

	Ref	Expression
Assertion	wl-sb9v	⊢ ( ∀ 𝑥 [ 𝑥 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		alcom	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
2		sb6	⊢ ( [ 𝑥 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) )
3		equcom	⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
4	3	imbi1i	⊢ ( ( 𝑦 = 𝑥 → 𝜑 ) ↔ ( 𝑥 = 𝑦 → 𝜑 ) )
5	4	albii	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) ↔ ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 ) )
6	2 5	bitri	⊢ ( [ 𝑥 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 ) )
7	6	albii	⊢ ( ∀ 𝑥 [ 𝑥 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 ) )
8		sb6	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
9	8	albii	⊢ ( ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
10	1 7 9	3bitr4i	⊢ ( ∀ 𝑥 [ 𝑥 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )