Theorem wl-sb8et

Description: Substitution of variable in universal quantifier. Closed form of sb8e . (Contributed by Wolf Lammen, 27-Jul-2019)

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

Proof

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