Theorem wl-sb8mot

Description: Substitution of variable in universal quantifier. Closed form of sb8mo . (Contributed by Wolf Lammen, 11-Aug-2019)

	Ref	Expression
Assertion	wl-sb8mot	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		wl-sb8et	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
2		wl-sb8eut	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
3	1 2	imbi12d	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ↔ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) ) )
4		moeu	⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
5		moeu	⊢ ( ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ↔ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
6	3 4 5	3bitr4g	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )