Theorem wl-sb8eft

Description: Substitution of variable in existentialal quantifier. Closed form of sb8ef . (Contributed by Wolf Lammen, 27-Apr-2025)

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

Proof

Step	Hyp	Ref	Expression
1		nfnt	⊢ ( Ⅎ 𝑦 𝜑 → Ⅎ 𝑦 ¬ 𝜑 )
2	1	alimi	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ∀ 𝑥 Ⅎ 𝑦 ¬ 𝜑 )
3		wl-sb8ft	⊢ ( ∀ 𝑥 Ⅎ 𝑦 ¬ 𝜑 → ( ∀ 𝑥 ¬ 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] ¬ 𝜑 ) )
4	2 3	syl	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∀ 𝑥 ¬ 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] ¬ 𝜑 ) )
5		alnex	⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
6		sbn	⊢ ( [ 𝑦 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝑦 / 𝑥 ] 𝜑 )
7	6	albii	⊢ ( ∀ 𝑦 [ 𝑦 / 𝑥 ] ¬ 𝜑 ↔ ∀ 𝑦 ¬ [ 𝑦 / 𝑥 ] 𝜑 )
8		alnex	⊢ ( ∀ 𝑦 ¬ [ 𝑦 / 𝑥 ] 𝜑 ↔ ¬ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
9	7 8	bitri	⊢ ( ∀ 𝑦 [ 𝑦 / 𝑥 ] ¬ 𝜑 ↔ ¬ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
10	4 5 9	3bitr3g	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ¬ ∃ 𝑥 𝜑 ↔ ¬ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
11	10	con4bid	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )